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.
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.
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.
M. Gordon & T. Melham (1993):
Introduction to HOL: A Theorem Proving Environment for Higher Order Logic.
Cambridge University Press.
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.
T. Hales (2015):
A Formal Proof of the Kepler Conjecture.
Preprint available at arxiv.org.
ArXiv:1501.02155v1 [math.MG].
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.
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.
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.
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.
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.
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.
L. Paulson (1987):
Logic and Computation: Interactive proof with Cambridge LCF.
Cambridge University Press,
doi:10.1017/CBO9780511526602.
K. Slind (1991):
An Implementation of Higher Order Logic.
Technical Report 91-419-03.
Computer Science Department, University of Calgary.
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.
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.