References

1. Martín Abadi & Leslie Lamport (1991): The Existence of Refinement Mappings. Journal of Theoretical Computer Science 82(2), doi:10.1016/0304-3975(91)90224-P.
2. Jean-Raymond Abrial (1996): The B-Book: Assigning Programs to Meanings. Cambridge University Press, doi:10.1017/CBO9780511624162.
3. The ACL2 Theorem Prover. http://www.cs.utexas.edu/~moore/acl2.
4. Peter B. Andrews (2002): An Introduction to Mathematical Logic and Type Theory: To Thruth Through Proof. Springer, doi:10.1007/978-94-015-9934-4.
5. R. S. Boyer, D. M. Goldschlag, M. Kaufmann & J S. Moore (1991): Functional Instantiation in First Order Logic. Technical Report 44. Computational Logic Inc..
6. Alonzo Church (1940): A Formulation of the Simple Theory of Types. The Journal of Symbolic Logic 5(2), doi:10.2307/2266170.
7. Michael Clarkson & Fred Schneider (2010): Hyperproperties. Journal of Computer Security 18(6), doi:10.3233/JCS-2009-0393.
8. Alessandro Coglio (2014): Pop-Refinement. Archive of Formal Proofs. http://afp.sf.net/entries/Pop_Refinement.shtml, Formal proof development.
9. Edsger W. Dijkstra (1968): A Constructive Approach to the Problem of Program Correctness. BIT 8(3), doi:10.1007/BF01933419.
10. Joseph Goguen & José Meseguer (1982): Security Policies and Security Models. In: Proc. IEEE Symposium on Security and Privacy, doi:10.1109/SP.1982.10014.
11. David Greve (2009): Automated Reasoning with Quantified Formulae. In: Proc. 8th International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2-2009), doi:10.1145/1637837.1637855.
12. C. A. R. Hoare (1972): Proof of Correctness of Data Representations. Acta Informatica 1(4), doi:10.1007/BF00289507.
13. Cliff Jones (1990): Systematic Software Development using VDM, second edition. Prentice Hall.
14. Sebastiaan J. C. Joosten, Bernard van Gastel & Julien Schmaltz (2013): A Macro for Reusing Abstract Functions and Theorems. In: Proc. 11th International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2-2013), doi:10.4204/EPTCS.114.3.
15. Matt Kaufmann & J Strother Moore (2001): Structured Theory Development for a Mechanized Logic, doi:10.1023/A:1026517200045.
16. Panagiotis Manolios & J Strother Moore (2003): Partial Functions in ACL2, doi:10.1023/B:JARS.0000009505.07087.34.
17. F. J. Martìn-Mateos, J. A. Alonso, M. J. Hidalgo & J. L. Ruiz-Reina (2002): A Generic Instantiation Tool and a Case Study: A Generic Multiset Theory. In: Proc. 3rd International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2-2002).
18. Robin Milner (1971): An Algebraic Definition of Simulation between Programs. Technical Report CS-205. Stanford University.
19. J Strother Moore (2009): Automatically Computing Functional Instantiations. In: Proc. 8th International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2-2009), doi:10.1145/1637837.1637839.
20. Carroll Morgan (1998): Programming from Specifications, second edition. Prentice Hall.
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. Sol Swords & Jared Davis (2015): Fix Your Types. In: Proc. 13th International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2-2015).

Comments and questions to: eptcs@eptcs.org

For website issues: webmaster@eptcs.org