Peter B. Andrews (1986):
An introduction to mathematical logic and type theory: to truth through proof.
Academic Press Professional, Inc.,
San Diego, CA, USA.
Andrew W. Appel (2001):
Foundational Proof-Carrying Code.
In: LICS.
IEEE Computer Society,
Washington, DC, USA,
pp. 247256,
doi:10.1109/LICS.2001.932501.
Ali Assaf & Raphaël Cauderlier (2015):
Mixing HOL and Coq in Dedukti (Rough Diamond).
Available at https://hal.inria.fr/hal-01141789.
To appear in PxTP 2015.
H. P. Barendregt (1992):
Lambda Calculi with Types, Handbook of Logic in Computer Science Vol. II.
Oxford University Press.
Michael Beeson (1985):
Foundations of Constructive Mathematics.
Springer-Verlag,
doi:10.1007/978-3-642-68952-9.
M. Boespflug & G. Burel (2012):
CoqInE: Translating the calculus of inductive constructions into the lambda-Pi-calculus modulo.
In: PxTP,
pp. 44–50.
M. Boespflug, Q. Carbonneaux & O. Hermant (2012):
The lambda-Pi-calculus modulo as a universal proof language.
In: PxTP,
pp. 28–43.
Zakaria Chihani, Dale Miller & Fabien Renaud (2013):
Foundational proof certificates in first-order Logic.
In: Maria Paola Bonacina: Automated Deduction CADE-24,
Lecture Notes in Computer Science 7898.
Springer Berlin Heidelberg,
pp. 162–177,
doi:10.1007/978-3-642-38574-2_11.
Alonzo Church (1940):
A formulation of the simple theory of types.
Journal of Symbolic Logic 5(02),
pp. 56–68,
doi:10.2307/2266170.
Denis Cousineau & Gilles Dowek (2007):
Embedding Pure Type Systems in the Lambda-Pi-Calculus Modulo.
In: Simona Ronchi Della Rocca: TLCA,
LNCS 4583.
Springer Berlin Heidelberg,
pp. 102–117,
doi:10.1007/978-3-540-73228-0_9.
Herman Geuvers (1993):
Logics and type systems.
PhD thesis.
University of Nijmegen.
Herman Geuvers & Erik Barendsen (1999):
Some logical and syntactical observations concerning the first-order dependent type system lambda-P.
Mathematical Structures in Computer Science 9(04),
pp. 335–359,
doi:10.1017/S0960129599002856.
Thomas C. Hales (2007):
The Jordan Curve Theorem, Formally and Informally.
American Mathematical Monthly 114(10),
pp. 882–894.
Thomas C. Hales, John Harrison, Sean McLaughlin, Tobias Nipkow, Steven Obua & Roland Zumkeller (2011):
A Revision of the Proof of the Kepler Conjecture.
In: Jeffrey C. Lagarias: The Kepler Conjecture.
Springer New York,
pp. 341–376,
doi:10.1007/978-1-4614-1129-1_9.
Robert Harper, Furio Honsell & Gordon Plotkin (1993):
A framework for defining logics.
J. ACM 40(1),
pp. 143184,
doi:10.1145/138027.138060.
Joe Hurd (2011):
The OpenTheory Standard Theory Library.
In: Mihaela Bobaru, Klaus Havelund, Gerard J. Holzmann & Rajeev Joshi: NFM,
LNCS 6617.
Springer,
pp. 177–191,
doi:10.1007/978-3-642-20398-5_14.
Cezary Kaliszyk & Alexander Krauss (2013):
Scalable LCF-Style Proof Translation.
In: Sandrine Blazy, Christine Paulin-Mohring & David Pichardie: ITP,
LNCS 7998.
Springer Berlin Heidelberg,
pp. 51–66,
doi:10.1007/978-3-642-39634-2_7.
Chantal Keller & Benjamin Werner (2010):
Importing HOL Light into Coq.
In: Matt Kaufmann & Lawrence C. Paulson: ITP,
LNCS 6172.
Springer Berlin Heidelberg,
pp. 307–322,
doi:10.1007/978-3-642-14052-5_22.
Dale Miller (1991):
Unification of simply typed lambda-terms as logic programming.
Technical Reports (CIS).
Dale A. Miller (2004):
Proofs in higher-order logic.
University of Pennsylvania.
Pavel Naumov, Mark-Oliver Stehr & José Meseguer (2001):
The HOL/NuPRL Proof Translator.
In: Richard J. Boulton & Paul B. Jackson: TPHOLs,
LNCS 2152.
Springer Berlin Heidelberg,
pp. 329–345,
doi:10.1007/3-540-44755-5_23.
Steven Obua & Sebastian Skalberg (2006):
Importing HOL into Isabelle/HOL.
In: Ulrich Furbach & Natarajan Shankar: Automated Reasoning,
LNCS 4130.
Springer Berlin Heidelberg,
pp. 298–302,
doi:10.1007/11814771_27.
Frank Pfenning & Carsten Schürmann (1999):
System Description: Twelf A Meta-Logical Framework for Deductive Systems.
In: CADE-16,
LNCS 1632.
Springer Berlin Heidelberg,
pp. 202–206,
doi:10.1007/3-540-48660-7_14.
Florian Rabe (2010):
Representing Isabelle in LF.
EPTCS 34,
pp. 85–99,
doi:10.4204/EPTCS.34.8.
arXiv: 1009.2794.
Florian Rabe & Michael Kohlhase (2013):
A scalable module system.
Inf. Comput. 230,
pp. 1–54,
doi:10.1016/j.ic.2013.06.001.
Carsten Schürmann & Mark-Oliver Stehr (2006):
An Executable Formalization of the HOL/Nuprl Connection in the Metalogical Framework Twelf.
In: Miki Hermann & Andrei Voronkov: LPAR,
LNCS 4246.
Springer Berlin Heidelberg,
pp. 150–166,
doi:10.1007/11916277_11.
Freek Wiedijk (2007):
The QED manifesto revisited.
Studies in Logic, Grammar and Rhetoric 10(23),
pp. 121–133.