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