Jean-Christophe Filli^atre (2000):
Design of a proof assistant: Coq version 7.
Research Report 1369.
LRI, Université Paris Sud.
Herman Geuvers, Robbert Krebbers, James McKinna & Freek Wiedijk (2010):
Pure Type Systems without Explicit Contexts.
In: Karl Crary & Marino Miculan: Proceedings 5th International Workshop on Logical Frameworks and Meta-languages: Theory and Practice,
Electronic Proceedings in Theoretical Computer Science 34,
pp. 53–67,
doi:10.4204/EPTCS.34.6.
Mike Gordon & Tom Melham (1993):
Introduction to HOL.
Cambridge University Press,
Cambridge.
Mike Gordon, Robin Milner & Christopher Wadsworth (1979):
Edinburgh LCF: A Mechanised Logic of Computation.
LNCS 78.
Springer Verlag,
Berlin, Heidelberg, New York.
Tom Hales (2007):
The Jordan Curve Theorem, Formally and Informally.
The American Mathematical Monthly 114,
pp. 882–894.
John Harrison (1996):
HOL Light: A Tutorial Introduction.
In: Mandayam Srivas & Albert Camilleri: Proceedings of the First International Conference on Formal Methods in Computer-Aided Design (FMCAD'96),
LNCS 1166.
Springer-Verlag,
pp. 265–269,
doi:10.1007/BFb0031814.
John Harrison (1999):
A Machine-Checked Theory of Floating Point Arithmetic.
In: Y. Bertot, G. Dowek, A. Hirschowitz, C. Paulin & L. Thery: Theorem Proving in Higher Order Logics: TPHOLs '99,
LNCS 1690,
pp. 113–130,
doi:10.1007/3-540-48256-3_9.
John Harrison (2000):
The HOL Light manual (1.1).
John Harrison (2006):
Floating-Point Verification using Theorem Proving.
In: Proceedings of SFM 2006, the 6th International School on Formal Methods for the Design of Computer, Communication, and Software Systems,
LNCS 2965,
pp. 211–242,
doi:10.1007/11757283_8.
John Harrison (2006):
Towards self-verification of HOL Light.
In: Ulrich Furbach & Natarajan Shankar: Proceedings of the Third International Joint Conference IJCAR 2006,
LNCS 4130.
Springer,
Seattle, WA,
pp. 177–191,
doi:10.1007/11814771_17.
John Harrison (2008):
Formalizing an Analytic Proof of the Prime Number Theorem.
In: R. Boulton, J. Hurd & K. Slind: Tools and Techniques for Verification of System Infrastructure.
The Royal Society,
pp. 243–261,
doi:10.1007/s10817-009-9145-6.
A. C. Leisenring (1969):
Mathematical logic and Hilbert's ε-symbol.
Macdonald.
Xavier Leroy (2008):
The Objective Caml system release 3.11, Documentation and user's manual.
Makarius Wenzel (2002):
The Isabelle/Isar Reference Manual.
TU München.
Freek Wiedijk (2010):
Pollack-inconsistency.
To be published in UITP 2010.
eptcs@eptcs.org