@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/},
)