@book(bmethod,
 author       = {Jean-Raymond Abrial},
 year         = {1996},
 title        = {The {B-Book}: Assigning Programs to Meanings},
 publisher    = {Cambridge University Press},
 doi          = {10.1017/CBO9780511624162},
)
@misc(acl2s,
 title        = {The {ACL2} Sedan},
 note         = {\url{http://acl2s.ccs.neu.edu/acl2s/doc/}},
)
@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(soft,
 author       = {Alessandro Coglio},
 year         = {2015},
 title        = {Second-Order Functions and Theorems in {ACL2}},
 booktitle    = {Proc.\ 13th International Workshop on the {ACL2} Theorem Prover and Its Applications ({ACL2-2015})},
 series       = {Electronic Proceedings in Theoretical Computer Science (EPTCS)},
 pages        = {17--33},
 doi          = {10.4204/EPTCS.192.3},
)
@inproceedings(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(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})},
 pages        = {125--141},
 doi          = {10.4204/EPTCS.327.12},
)
@inproceedings(13-davis-embedding,
 author       = {Jared Davis},
 year         = {2013},
 title        = {Embedding {ACL2} Models in End-User Applications},
 booktitle    = {Proc.\ 11th International Workshop on the {ACL2} Theorem Prover and its Applications ({ACL2-2013})},
 pages        = {2--4},
)
@article(dijkstra-constructive,
 author       = {Edsger W.\ Dijkstra},
 year         = {1968},
 title        = {A Constructive Approach to the Problem of Program Correctness},
 journal      = {BIT},
 volume       = {8},
 number       = {3},
 doi          = {10.1007/BF01933419},
)
@misc(docker-engine,
 title        = {Docker Engine},
 note         = {\url{https://www.docker.com/products/container-runtime/}},
)
@misc(gamboa-jupyter,
 author       = {Ruben Gamboa},
 title        = {Jupyter Kernel for {ACL2}: Source Code},
 note         = {\url{https://github.com/rubengamboa/acl2_jupyter}},
)
@article(embedded-dsl,
 author       = {Paul Hudak},
 year         = {1996},
 title        = {Building Domain-Specific Embedded Languages},
 journal      = {{ACM} Computing Surveys},
 volume       = {28},
 number       = {4es},
 doi          = {10.1145/242224.242477},
)
@book(vdm,
 author       = {Cliff Jones},
 year         = {1990},
 title        = {Systematic Software Development using {VDM}},
 edition      = {second},
 publisher    = {Prentice Hall},
)
@misc(acl2-www,
 author       = {Matt Kaufmann and J Strother Moore},
 title        = {The {ACL2} Theorem Prover},
 note         = {\url{http://acl2.org}},
)
@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}},
)
@article(PER-GRA:2007,
 author       = {Fernando P\'erez and Brian E. Granger},
 year         = {2007},
 title        = {{IP}ython: A System for Interactive Scientific Computing},
 journal      = {Computing in Science and Engineering},
 volume       = {9},
 number       = {3},
 pages        = {21--29},
 doi          = {10.1109/MCSE.2007.53},
 url          = {https://ipython.org},
)
@article(kids,
 author       = {Douglas R. Smith},
 year         = {1990},
 title        = {{KIDS}: A Semi-Automatic Program Development System},
 journal      = {IEEE Transactions on Software Engineering --- Special Issue on Formal Methods},
 volume       = {16},
 number       = {9},
 pages        = {1024--1043},
 doi          = {10.1109/32.58788},
)
@book(zed,
 author       = {J. M. Spivey},
 year         = {1992},
 title        = {The {Z} Notation: A Reference Manual},
 edition      = {second},
 publisher    = {Prentice Hall},
)
@misc(pvs-www,
 author       = {{SRI International}},
 title        = {{PVS}},
 note         = {\url{http://pvs.csl.sri.com}},
)
@inproceedings(15-swords-fty,
 author       = {Sol Swords and Jared Davis},
 year         = {2015},
 title        = {Fix Your Types},
 booktitle    = {Proc.\ 13th International Workshop on the {ACL2} Theorem Prover and its Applications ({ACL2-2015})},
 pages        = {3--16},
 doi          = {10.4204/EPTCS.192.2},
)
@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}},
)
@misc(vscode,
 title        = {Visual Studio Code},
 note         = {\url{https://code.visualstudio.com/}},
)
@misc(xtext,
 title        = {Xtext},
 note         = {\url{https://www.eclipse.org/Xtext/}},
)