Engineering formal metatheory, pp.3-15, 2008. ,
DOI : 10.1145/1328438.1328443
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.103.5948
The Coq proof assistant: reference manual, 2000. ,
URL : https://hal.archives-ouvertes.fr/inria-00069968
An inverse of the evaluation functional for typed lambda -calculus, [1991] Proceedings Sixth Annual IEEE Symposium on Logic in Computer Science, pp.203-211, 1991. ,
DOI : 10.1109/LICS.1991.151645
Proof Terms for Simply Typed Higher Order Logic, pp.38-52 ,
DOI : 10.1007/3-540-44659-1_3
A Prototype Proof Translator from HOL to Coq, pp.108-125 ,
DOI : 10.1007/3-540-44659-1_8
Type-safe modular hash-consing, Proceedings of the 2006 workshop on ML , ML '06, pp.12-19, 2006. ,
DOI : 10.1145/1159876.1159880
Automated Reasoning, Third International Joint Conference Proceedings, Lecture Notes in Computer Science, 2006. ,
DOI : 10.1007/11814771
Simple Types in Type Theory: Deep and Shallow Encodings, TPHOLs. Lecture Notes in Computer Science, vol.4732, pp.368-382, 2007. ,
DOI : 10.1007/978-3-540-74591-4_27
A Small Scale Reflection Extension for the Coq system, Tech. rep, 2007. ,
URL : https://hal.archives-ouvertes.fr/inria-00258384
Introduction to HOL: A theorem proving environment for higher order logic, 1993. ,
HOL Light: A tutorial introduction, Lecture Notes in Computer Science, vol.1166, pp.265-269, 1996. ,
DOI : 10.1007/BFb0031814
Towards Self-verification of HOL Light, pp.177-191 ,
DOI : 10.1007/11814771_17
OpenTheory: Package Management for Higher Order Logic Theories, p.31, 2009. ,
Importing HOL into Isabelle/HOL, pp.298-302 ,
DOI : 10.1007/11814771_27
Encoding the HOL Light logic in Coq, 2007. ,
Recording and checking HOL proofs, Lecture Notes in Computer Science, vol.971, pp.353-368, 1995. ,
DOI : 10.1007/3-540-60275-5_76
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.54.6141
A comparative study of Coq and HOL, Lecture Notes in Computer Science, vol.1275, pp.323-337, 1997. ,
DOI : 10.1007/BFb0028403