@book(bmethod,
 author       = {Jean-Raymond Abrial},
 year         = {1996},
 title        = {The {B-Book}: Assigning Programs to Meanings},
 publisher    = {Cambridge University Press},
 doi          = {10.1017/CBO9780511624162},
)
@article(popref,
 author       = {Alessandro Coglio},
 year         = {2014},
 title        = {Pop-Refinement},
 journal      = {Archive of Formal Proofs},
 note         = {\url{http://afp.sf.net/entries/Pop_Refinement.shtml}, Formal proof development},
)
@inproceedings(atj-deep,
 author       = {Alessandro Coglio},
 year         = {2018},
 title        = {A Simple Java Code Generator for {ACL2} Based on a Deep Embedding of {ACL2} in {Java}},
 booktitle    = {Proc.\ 15th International Workshop on the {ACL2} Theorem Prover and Its Applications ({ACL2-2018})},
 series       = {Electronic Proceedings in Theoretical Computer Science (EPTCS)},
 volume       = {280},
 pages        = {1--17},
 doi          = {10.4204/EPTCS.280.1},
)
@inproceedings(atj-shallow,
 author       = {Alessandro Coglio},
 year         = {2022},
 title        = {A Complex {Java} Code Generator for {ACL2} Based on a Shallow Embedding of {ACL2} in {Java}},
 booktitle    = {Proc.\ 17th International Workshop on the {ACL2} Theorem Prover and Its Applications ({ACL2-2022})},
)
@inproceedings(apt-simplify,
 author       = {Alessandro Coglio and Matt Kaufmann and Eric Smith},
 year         = {2017},
 title        = {A Versatile, Sound Tool for Simplifying Definitions},
 booktitle    = {Proc.\ 14th International Workshop on the {ACL2} Theorem Prover and Its Applications ({ACL2-2017})},
 pages        = {61--77},
 doi          = {10.4204/EPTCS.249.5},
)
@inproceedings(apt-isodata,
 author       = {Alessandro Coglio and Stephen Westfold},
 year         = {2020},
 title        = {Isomorphic Data Type Transformations},
 booktitle    = {Proc.\ 16th International Workshop on the {ACL2} Theorem Prover and Its Applications ({ACL2-2020})},
 series       = {Electronic Proceedings in Theoretical Computer Science (EPTCS)},
 volume       = {327},
 pages        = {125--141},
 doi          = {10.4204/EPTCS.280.1},
)
@misc(coq-refman,
 title        = {Coq 8.15.0 Reference Manual},
 howpublished = {\url{https://coq.inria.fr}},
)
@inproceedings(c-k,
 author       = {Chucky Ellison and Grigore Rosu},
 year         = {2012},
 title        = {An Executable Formal Semantics of {C} with Applications},
 booktitle    = {Proc.\ 39th {ACM SIGPLAN} Symposium on Principles of Programming Languages ({POPL})},
 pages        = {533--544},
 doi          = {10.1145/2103656.2103719},
)
@misc(isa-codegen,
 author       = {{Florian Haftmann with contributions from Lukas Bulwahn}},
 year         = {2021},
 title        = {Code generation from Isabelle/HOL theories},
 howpublished = {\url{https://isabelle.in.tum.de}},
 note         = {Tutorial distributed with Isabelle/HOL},
)
@inproceedings(c-asm,
 author       = {Yuri Gurevich and James K. Huggins},
 year         = {1992},
 title        = {The Semantics of the {C} Programming Language},
 booktitle    = {Proc.\ 6th International Workshop on Computer Science Logic ({CSL})},
 series       = {Lecture Notes in Computer Science (LNCS)},
 volume       = {702},
 pages        = {274--308},
 doi          = {10.1007/3-540-56992-8_17},
)
@techreport(c18,
 author       = {{ISO/IEC}},
 year         = {2018},
 title        = {{ISO/IEC} 9899: Information Technology --- Programming Languages --- {C}},
 type         = {International Standard},
 note         = {Fourth Edition},
)
@book(vdm,
 author       = {Cliff Jones},
 year         = {1990},
 title        = {Systematic Software Development using {VDM}},
 edition      = {second},
 publisher    = {Prentice Hall},
)
@book(parteval,
 author       = {Neil D. Jones and Carsten K. Gomard and Peter Sestoft},
 year         = {1999},
 title        = {Partial Evaluation and Automatic Program Generation},
 publisher    = {Prentice Hall},
 note         = {\url{http://www.itu.dk/people/sestoft/pebook}},
)
@misc(apt-www,
 author       = {{Kestrel Institute}},
 title        = {{APT (Automated Program Transformations)}},
 howpublished = {\url{https://www.kestrel.edu/research/apt}},
)
@misc(specware-www,
 author       = {{Kestrel Institute}},
 title        = {{Specware}},
 note         = {\url{https://www.kestrel.edu/research/specware}},
)
@article(c-coq,
 author       = {Xavier Leroy},
 year         = {2009},
 title        = {Mechanized semantics for the {Clight} subset of the {C} language},
 journal      = {Journal of Automated Reasoning (JAR)},
 volume       = {43},
 number       = {3},
 pages        = {263--288},
 doi          = {10.1007/s10817-009-9148-3},
)
@phdthesis(c-hol,
 author       = {Michael Norrish},
 year         = {1998},
 title        = {{C} formalised in {HOL}},
 school       = {University of Cambridge},
)
@phdthesis(c-papaspyrou,
 author       = {Nikolaos S. Papaspyrou},
 year         = {1998},
 title        = {A Formal Semantics for the {C} Programming Language},
 school       = {National Technical University of Athens},
)
@book(russinoff-book,
 author       = {David M. Russinoff},
 year         = {2022},
 title        = {Formal Verification of Floating-Point Hardware Design},
 edition      = {2nd},
 publisher    = {Springer},
 doi          = {10.1007/978-3-030-87181-9},
)
@inproceedings(pvs-codegen,
 author       = {Nararajan Shankar},
 year         = {2017},
 title        = {A Brief Introduction to the {PVS2C} Code Generator},
 booktitle    = {Proc.\ Workshop on Automated Formal Methods ({AFM'17})},
)
@book(zed,
 author       = {J. M. Spivey},
 year         = {1992},
 title        = {The {Z} Notation: A Reference Manual},
 edition      = {second},
 publisher    = {Prentice Hall},
)
@misc(acl2-manual,
 author       = {{The ACL2 Community}},
 title        = {The {ACL2} Theorem Prover and Community Books: Documentation},
 note         = {\url{http://acl2.org/manual}},
)