References

1. M. Adams & P. Clayton (2005): ClawZ: Cost-Effective Formal Verification for Control Systems. In: Proceedings of the 7th International Conference on Formal Methods and Software Engineering, Lecture Notes in Computer Science 3785. Springer, pp. 465–479, doi:10.1007/11576280_32.
2. M. Adams (2015): Proof Auditing Formalised Mathematics. Available at http://www.proof-technologies.com/flyspeck/qed_paper.pdf. Accepted for publication in the Journal of Formalized Reasoning.
3. R. Arthan & R. Jones (2005): Z in HOL in ProofPower. In Issue 2005-1 of the British Computer Society Specialist Group Newsletter on Formal Aspects of Computing Science.
4. R. Arthan (2014): HOL Constant Definition Done Right. In: Proceedings of the 5th International Conference on Interactive Theorem Proving, Lecture Notes in Computer Science 8558. Springer, pp. 531–536, doi:10.1007/978-3-319-08970-6_34.
5. M. Gordon & T. Melham (1993): Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press.
6. M. Gordon, R. Milner & C. Wadsworth (1979): Edinburgh LCF: A Mechanised Logic of Computation. Lecture Notes in Computer Science 78. Springer, doi:10.1007/3-540-09724-4.
7. T. Hales (2015): A Formal Proof of the Kepler Conjecture. Preprint available at arxiv.org. ArXiv:1501.02155v1 [math.MG].
8. J. Harrison (2009): HOL Light: An Overview. In: Proceedings of the 22nd International Conference on Theorem Proving in Higher Order Logics, Lecture Notes in Computer Science 5674. Springer, pp. 60–66, doi:10.1007/978-3-642-03359-9_4.
9. J. Hurd (2011): The OpenTheory Standard Theory Library. In: Proceedings of the Third International Symposium on NASA Formal Methods, Lecture Notes in Computer Science 6617. Springer, pp. 177–191, doi:10.1007/978-3-642-20398-5_14.
10. C. Kaliszyk & A. Krauss (2013): Scalable LCF-Style Proof Translation. In: Proceedings of the 4th International Conference on Interactive Theorem Proving, Lecture Notes in Computer Science 7998. Springer, pp. 51–66, doi:10.1007/978-3-642-39634-2_7.
11. G. Klein (2009): seL4: Formal Verification of an OS Kernel. In: Proceedings of the ACM SIGOPS 22nd Symposium on Operating Systems Principles. ACM, pp. 207–220, doi:10.1145/1629575.1629596.
12. T. Nipkow, L. Paulson & M. Wenzel (2002): Isabelle/HOL: A Proof Assistant for Higher-Order Logic. Lecture Notes in Computer Science 2283. Springer, doi:10.1007/3-540-45949-9.
13. S. Obua & S. Skalberg (2006): Importing HOL into Isabelle/HOL. In: Proceedings of the Third International Joint Conference on Automated Reasoning, Lecture Notes in Computer Science 4130. Springer, pp. 298–302, doi:10.1007/11814771_27.
14. L. Paulson (1987): Logic and Computation: Interactive proof with Cambridge LCF. Cambridge University Press, doi:10.1017/CBO9780511526602.
15. K. Slind (1991): An Implementation of Higher Order Logic. Technical Report 91-419-03. Computer Science Department, University of Calgary.
16. K. Slind & M. Norrish (2008): A Brief Overview of HOL4. In: Proceedings of the 21st International Conference on Theorem Proving in Higher Order Logics, Lecture Notes in Computer Science 5170. Springer, pp. 28–32, doi:10.1007/978-3-540-71067-7_6.
17. M. Wenzel, L. Paulson & T. Nipkow (2008): The Isabelle Framework. In: Proceedings of the 21st International Conference on Theorem Proving in Higher Order Logics, Lecture Notes in Computer Science 5170. Springer, pp. 33–38, doi:10.1007/978-3-540-71067-7_7.
18. HOL Light adaptation for Common HOL. Available at http://www.proof-technologies.com/commonhol/commonhol-0.5-hl-svn197.tgz.
19. HOL Zero homepage. Available at http://www.proof-technologies.com/holzero/.

Comments and questions to: eptcs@eptcs.org

For website issues: webmaster@eptcs.org