Alessandro Coglio (2015):
Second-Order Functions and Theorems in ACL2.
In: Proc. 13th International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2-2015),
Electronic Proceedings in Theoretical Computer Science (EPTCS),
pp. 17–33,
doi:10.4204/EPTCS.192.3.
Alessandro Coglio (2018):
A Simple Java Code Generator for ACL2 Based on a Deep Embedding of ACL2 in Java.
In: Proc. 15th International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2-2018),
Electronic Proceedings in Theoretical Computer Science (EPTCS),
pp. 1–17,
doi:10.4204/EPTCS.280.1.
Alessandro Coglio, Matt Kaufmann & Eric Smith (2017):
A Versatile, Sound Tool for Simplifying Definitions.
In: Proc. 14th International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2-2017),
pp. 61–77,
doi:10.4204/EPTCS.249.5.
Cyrill Cohen, Maxime Dénès & Anders Mörtberg (2013):
Refinements for Free!.
In: Proc. 3d International Conference on Certified Programs and Proofs (CPP),
LNCS 8307.
Springer,
pp. 147–162,
doi:10.1007/978-3-319-03545-1_10.
Benjamin Delaware, Clement Pit-Claudel, Jason Gross & Adam Chlipala (2015):
Fiat: Deductive Synthesis of Abstract Data Types in a Proof Assistant.
In: Proc. 42nd ACM Symposium on Principles of Programming Languages (POPL),
doi:10.1145/2676726.2677006.
Edsger W. Dijkstra (1968):
A Constructive Approach to the Problem of Program Correctness.
BIT 8(3),
doi:10.1007/BF01933419.
Cordell Green (2014):
The `Analysis-By-Synthesis' Idea.
Private Communication.
C. A. R. Hoare (1972):
Proof of Correctness of Data Representations.
Acta Informatica 1(4),
pp. 271–281,
doi:10.1007/BF00289507.
Cliff Jones (1990):
Systematic Software Development using VDM,
second edition.
Prentice Hall.
Peter Lammich (2019):
Refinement to Imperative HOL.
Journal of Automated Reasoning 62(4),
pp. 481–503,
doi:10.1007/s10817-017-9437-1.
Andreas Lochbihler (2013):
Light-weight containers for Isabelle: Efficient, Extensible, Nestable.
In: Proc. 4th International Conference on Interactive Theorem Proving (ITP),
LNCS 7998.
Springer,
pp. 116–132,
doi:10.1007/978-3-642-39634-2_11.
Douglas R. Smith (1990):
KIDS: A Semi-Automatic Program Development System.
IEEE Transactions on Software Engineering — Special Issue on Formal Methods 16(9),
pp. 1024–1043,
doi:10.1109/32.58788.
Douglas R. Smith (1993):
Constructing Specification Morphisms.
Journal of Symbolic Computation, Special Issue on Automatic Programming 15(5–6),
pp. 571–606,
doi:10.1016/S0747-7171(06)80006-4.
Douglas R. Smith (1999):
Mechanizing the Development of Software.
In: Manfred Broy: Calculational System Design, Proc. Marktoberdorf Summer School.
IOS Press.
J. M. Spivey (1992):
The Z Notation: A Reference Manual,
second edition.
Prentice Hall.
The ACL2 Community:
The ACL2 Theorem Prover and Community Books: Documentation.
http://www.cs.utexas.edu/~moore/acl2/manuals/current/manual.
Niklaus Wirth (1971):
Program Development by Stepwise Refinement.
Communications of the ACM 14(4),
pp. 221–227,
doi:10.1145/362575.362577.