@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(defiso-design-notes,
 author       = {Alessandro Coglio},
 title        = {Design Notes for \texttt{defiso}},
 note         = {\url{http://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/res/kestrel-std-util-design-notes/defiso.pdf}},
)
@misc(isodata-design-notes,
 author       = {Alessandro Coglio},
 title        = {Design Notes for \texttt{isodata}},
 note         = {\url{http://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/res/kestrel-apt-design-notes/isodata.pdf}},
)
@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(aij-atj,
 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)},
 pages        = {1--17},
 doi          = {10.4204/EPTCS.280.1},
)
@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(coq-eal,
 author       = {Cyrill Cohen and Maxime D\'en\`es and Anders M\"ortberg},
 year         = {2013},
 title        = {Refinements for Free!},
 booktitle    = {Proc.\ 3d International Conference on Certified Programs and Proofs ({CPP})},
 series       = {LNCS},
 volume       = {8307},
 publisher    = {Springer},
 pages        = {147--162},
 doi          = {10.1007/978-3-319-03545-1_10},
)
@inproceedings(coq-fiat,
 author       = {Benjamin Delaware and Pit-Claudel, Clement and Jason Gross and Adam Chlipala},
 year         = {2015},
 title        = {{Fiat}: Deductive Synthesis of Abstract Data Types in a Proof Assistant},
 booktitle    = {Proc.\ 42nd {ACM} Symposium on Principles of Programming Languages ({POPL})},
 doi          = {10.1145/2676726.2677006},
)
@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(analysis-by-synthesis,
 author       = {Cordell Green},
 year         = {2014},
 title        = {The `Analysis-By-Synthesis' Idea},
 howpublished = {Private Communication},
)
@article(hoare-data,
 author       = {C. A. R. Hoare},
 year         = {1972},
 title        = {Proof of Correctness of Data Representations},
 journal      = {Acta Informatica},
 volume       = {1},
 number       = {4},
 pages        = {271--281},
 doi          = {10.1007/BF00289507},
)
@book(vdm,
 author       = {Cliff Jones},
 year         = {1990},
 title        = {Systematic Software Development using {VDM}},
 edition      = {second},
 publisher    = {Prentice Hall},
)
@misc(apt-www,
 author       = {{Kestrel Institute}},
 title        = {{APT}},
 howpublished = {\url{https://www.kestrel.edu/home/projects/apt}},
)
@misc(derivationminer-www,
 author       = {{Kestrel Institute}},
 title        = {{DerivationMiner}},
 howpublished = {\url{https://www.kestrel.edu/home/projects/derivationminer}},
)
@misc(specware-www,
 author       = {{Kestrel Institute}},
 title        = {{Specware}},
 note         = {\url{http://www.specware.org}},
)
@article(isa-sepref,
 author       = {Peter Lammich},
 year         = {2019},
 title        = {Refinement to {Imperative HOL}},
 journal      = {Journal of Automated Reasoning},
 volume       = {62},
 number       = {4},
 pages        = {481--503},
 doi          = {10.1007/s10817-017-9437-1},
)
@inproceedings(isa-containers,
 author       = {Andreas Lochbihler},
 year         = {2013},
 title        = {Light-weight containers for {Isabelle}: Efficient, Extensible, Nestable},
 booktitle    = {Proc.\ 4th International Conference on Interactive Theorem Proving ({ITP})},
 series       = {LNCS},
 volume       = {7998},
 publisher    = {Springer},
 pages        = {116--132},
 doi          = {10.1007/978-3-642-39634-2_11},
)
@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},
)
@article(smith-connections,
 author       = {Douglas R.\ Smith},
 year         = {1993},
 title        = {Constructing Specification Morphisms},
 journal      = {Journal of Symbolic Computation, Special Issue on Automatic Programming},
 volume       = {15},
 number       = {5--6},
 pages        = {571--606},
 doi          = {10.1016/S0747-7171(06)80006-4},
)
@inproceedings(smith-marktoberdorf,
 author       = {Douglas R.\ Smith},
 year         = {1999},
 title        = {Mechanizing the Development of Software},
 editor       = {Manfred Broy},
 booktitle    = {Calculational System Design, Proc.\ Marktoberdorf Summer School},
 publisher    = {IOS Press},
)
@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://www.cs.utexas.edu/~moore/acl2/manuals/current/manual}},
)
@article(wirth-refinement,
 author       = {Niklaus Wirth},
 year         = {1971},
 title        = {Program Development by Stepwise Refinement},
 journal      = {Communications of the ACM},
 volume       = {14},
 number       = {4},
 pages        = {221--227},
 doi          = {10.1145/362575.362577},
)