References

1. Jean-Raymond Abrial (1996): The B-Book: Assigning Programs to Meanings. Cambridge University Press, doi:10.1017/CBO9780511624162.
2. Alessandro Coglio: Design Notes for defiso. http://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/res/kestrel-std-util-design-notes/defiso.pdf.
3. Alessandro Coglio: Design Notes for isodata. http://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/res/kestrel-apt-design-notes/isodata.pdf.
4. Alessandro Coglio (2014): Pop-Refinement. Archive of Formal Proofs. http://afp.sf.net/entries/Pop_Refinement.shtml, Formal proof development.
5. 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.
6. 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.
7. 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.
8. 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.
9. 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.
10. Edsger W. Dijkstra (1968): A Constructive Approach to the Problem of Program Correctness. BIT 8(3), doi:10.1007/BF01933419.
11. Cordell Green (2014): The `Analysis-By-Synthesis' Idea. Private Communication.
12. C. A. R. Hoare (1972): Proof of Correctness of Data Representations. Acta Informatica 1(4), pp. 271–281, doi:10.1007/BF00289507.
13. Cliff Jones (1990): Systematic Software Development using VDM, second edition. Prentice Hall.
14. Kestrel Institute: APT. https://www.kestrel.edu/home/projects/apt.
15. Kestrel Institute: DerivationMiner. https://www.kestrel.edu/home/projects/derivationminer.
16. Kestrel Institute: Specware. http://www.specware.org.
17. Peter Lammich (2019): Refinement to Imperative HOL. Journal of Automated Reasoning 62(4), pp. 481–503, doi:10.1007/s10817-017-9437-1.
18. 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.
19. 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.
20. 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.
21. Douglas R. Smith (1999): Mechanizing the Development of Software. In: Manfred Broy: Calculational System Design, Proc. Marktoberdorf Summer School. IOS Press.
22. J. M. Spivey (1992): The Z Notation: A Reference Manual, second edition. Prentice Hall.
23. The ACL2 Community: The ACL2 Theorem Prover and Community Books: Documentation. http://www.cs.utexas.edu/~moore/acl2/manuals/current/manual.
24. Niklaus Wirth (1971): Program Development by Stepwise Refinement. Communications of the ACM 14(4), pp. 221–227, doi:10.1145/362575.362577.

Comments and questions to: eptcs@eptcs.org

For website issues: webmaster@eptcs.org