@book(bmethod,
 author       = {Jean-Raymond Abrial},
 year         = {1996},
 title        = {The {B-Book}: Assigning Programs to Meanings},
 publisher    = {Cambridge University Press},
 doi          = {10.1017/CBO9780511624162},
)
@inproceedings(k-java,
 author       = {Bogd{\u a}na{\c s}, Denis and Ro{\c s}u, Grigore},
 year         = {2015},
 title        = {{K-Java}: A Complete Semantics of {Java}},
 booktitle    = {Proc.\ 42nd {ACM} Symposium on Principles of Programming Languages ({POPL})},
 pages        = {445--456},
 doi          = {10.1145/2676726.2676982},
)
@inproceedings(lec-monitors,
 author       = {Darren Cofer and Isaac Amundson and Ramachandra Sattigeri and Arjun Passi and Christopher Boggs and Eric Smith and Limei Gilham and Taejoon Byun and Sanjai Rayadurgam},
 year         = {2020},
 title        = {Run-Time Assurance for Learning-Based Aircraft Taxiing},
 booktitle    = {Proc.\ 39th Digital Avionics Systems Conference ({DASC})},
 doi          = {10.1109/DASC50938.2020.9256581},
)
@inproceedings(abnf,
 author       = {Alessandro Coglio},
 year         = {2018},
 title        = {A Formalization of the {ABNF} Notation and a Verified Parser of {ABNF} Grammars},
 booktitle    = {Proc.\ 10th Working Conference on Verified Software: Theories, Tools, and Experiments ({VSTTE})},
 series       = {Lecture Notes in Computer Science (LNCS)},
 volume       = {11294},
 pages        = {177--195},
 doi          = {10.1007/978-3-030-03592-1_10},
)
@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(atc,
 author       = {Alessandro Coglio},
 year         = {2022},
 title        = {A Proof-Generating {C} Code Generator for {ACL2} Based on a Shallow Embedding of {C} in {ACL2}},
 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})},
 series       = {Electronic Proceedings in Theoretical Computer Science (EPTCS)},
 volume       = {259},
 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}},
)
@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},
)
@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}},
 howpublished = {\url{https://www.kestrel.edu/research/apt}},
)
@misc(specware-www,
 author       = {{Kestrel Institute}},
 title        = {{Specware}},
 note         = {\url{https://www.kestrel.edu/research/specware}},
)
@inproceedings(java-light,
 author       = {Tobias Nipkow and David von Oheimb},
 year         = {1998},
 title        = {Java Light is Type-Safe --- Definitely},
 booktitle    = {Proc.\ 25th {ACM} Symposium on Principles of Programming Languages ({POPL})},
 pages        = {161--170},
 doi          = {10.1145/268946.268960},
)
@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},
)
@book(jbook,
 author       = {Robert St{\"a}rk and Joachim Schmid and Egon B{\"o}rger},
 year         = {2001},
 title        = {{Java} and the {Java} Virtual Machine: Definition, Verification, Validation},
 publisher    = {Springer},
 doi          = {10.1007/978-3-642-59495-3},
)
@misc(acl2-manual,
 author       = {{The ACL2 Community}},
 title        = {The {ACL2} Theorem Prover and Community Books: Documentation},
 note         = {\url{http://acl2.org/manual}},
)
@misc(acl2-code,
 author       = {{The ACL2 Community}},
 title        = {The {ACL2} Theorem Prover and Community Books: Source Code},
 note         = {\url{http://github.com/acl2/acl2}},
)