P.B. Andrews (1963):
A reduction of the axioms for the theory of propositional types.
Fundam. Math. 52,
pp. 345–350,
doi:10.4064/fm-52-3-345-350.
P.B. Andrews (1986):
An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof.
Academic Press.
A. Assaf (2014):
A Calculus of Constructions with explicit subtyping.
In: H. Herbelin, P. Letouzey & M. Sozeau: Types,
LIPICS 39,
pp. 27–46,
doi:10.4230/LIPIcs.TYPES.2014.27.
A. Assaf (2015):
A framework for defining computational higher-order logics.
École polytechnique.
A. Assaf, G. Burel, R. Cauderlier, D. Delahaye, G. Dowek, C. Dubois, F. Gilbert, P. Halmagrand, O. Hermant & R. Saillard (2016):
Dedukti: a Logical Framework based on the lambda-Pi-Calculus Modulo Theory.
Manuscript.
H. Barendregt (1992):
Lambda calculi with types.
In: S. Abramsky, D.M. Gabbay & T.S.E. Maibaum: Handbook of Logic in Computer Science 2.
Oxford University Press,
pp. 117–309.
M. Boespflug (2011):
Conception d'un noyau de vérification de preuves pour le lambda-Pi-calcul modulo.
École polytechnique.
M. Boespflug & G. Burel (2012):
CoqInE : Translating the Calculus of Inductive Constructions into the lambda-Pi-calculus modulo.
In: Second International Workshop on Proof Exchange for Theorem Proving,
pp. 44–50.
R. Cauderlier (2017):
A Rewrite System for Proof Constructivization.
https://who.rocq.inria.fr/Raphael.Cauderlier/constructivization.pdf.
R. Cauderlier & C. Dubois (2017):
FoCaLiZe and Dedukti to the Rescue for Proof Interoperability.
In: M. Ayala-Rincón & C.A. Muñoz: Interactive Theorem Proving,
Lecture Notes in Computer Science 10499.
Springer,
pp. 131–147,
doi:10.1007/11916277_11.
A. Church (1940):
A formulation of the simple theory of types.
The Journal of Symbolic Logic 5(2),
pp. 56–68,
doi:10.2307/2371199.
T. Coquand & G. Huet (1988):
The Calculus of Constructions.
Information and Computation,
pp. 95–120,
doi:10.1016/0890-5401(88)90005-3.
D. Cousineau & G. Dowek (2007):
Embedding Pure Type Systems in the lambda-Pi-calculus modulo.
In: S. Ronchi Della Rocca: Typed lambda calculi and applications,
Lecture Notes in Computer Science 4583.
Springer,
pp. 102–117,
doi:10.1007/978-3-540-73228-0_9.
G. Dowek (2015):
On the definition of the classical connectives and quantifiers.
In: E.H. Haeusler, W. de Campos Sanz & B. Lopes: Why is this a Proof?, Festschrift for Luiz Carlos Pereira.
College Publications.
G. Dowek, Th. Hardin & C. Kirchner (2001):
HOL-lambda-sigma: an intentional first-order expression of higher-order logic.
Mathematical Structures in Computer Science 11,
pp. 1–25,
doi:10.1017/S0960129500003236.
G. Dowek, Th. Hardin & C. Kirchner (2003):
Theorem proving modulo.
Journal of Automated Reasoning 31,
pp. 33–72,
doi:10.1023/A:1027357912519.
G. Dowek & B. Werner (2003):
Proof normalization modulo.
The Journal of Symbolic Logic 68(4),
pp. 1289–1316,
doi:10.1007/BFb0037116.
H. Friedman (1976):
Systems of second-order arithmetic with restricted induction, I, II.
The Journal of Symbolic Logic 41(2),
pp. 557–559.
H. Geuvers (1993):
Logics and Type systems.
Nijmegen.
H. Geuvers (1995):
The Calculus of Constructions and Higher Order Logic.
In: Ph. de Groote: The Curry-Howard isomorphism,
Cahiers du Centre de logique 8.
Université catholique de Louvain,
pp. 139–191.
F. Gilbert (2017):
Automated Constructivization of Proofs.
In: J. Esparza & A.S. Murawski: Foundations of Software Science and Computation Structures,
Lecture notes in computer science 10203.
Springer,
pp. 480–495,
doi:10.1007/978-3-540-71070-7_23.
J.-Y. Girard (1993):
On the Unity of Logic.
Annals of Pure and Applied Logic 59(3),
pp. 201–217,
doi:10.1016/0168-0072(93)90093-S.
R. Harper, F. Honsell & G. Plotkin (1993):
A framework for defining logics.
Journal of the ACM 40(1),
pp. 143–184,
doi:10.1145/138027.138060.
L. Henkin (1960):
On Mathematical Induction.
The American Mathematical Monthly 67(4),
pp. 323–338,
doi:10.2307/2308975.
L. Henkin (1963):
A theory of propositional types.
Fundam. Math. 52,
pp. 323–344,
doi:10.4064/fm-52-3-323-344.
Errata Ibid., 53, 119, 1964.
B. Huffman & Kunçar (2013):
Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL.
In: G. Gonthier & M. Norrish: Certified Programs and Proofs,
pp. 131–146,
doi:10.1007/978-3-319-03545-1_9.
J. Hurd (2011):
The OpenTheory standard theory library.
In: M. Bobaru, K. Havelund, G.J. Holzmann & R. Joshi: NASA Formal Methods,
Lecture Notes in Computer Science 6617.
Springer,
pp. 177–191,
doi:10.1007/3-540-60275-5_76.
F. Kirchner (2006):
A Finite First-Order Theory of Classes.
In: Th. Altenkirch & C. McBride: Types for Proofs and Programs,
Lecture Notes in Computer Science.
Springer,
pp. 188–202.
A. Leitsch (2015):
On proof mining by cut-elimination.
In: D. Delahaye & B. Woltzenlogel Paleo: All about Proofs, Proofs for All,
Mathematical Logic and Foundations 55.
College Publications,
pp. 173–200.
B. Nordström, K. Petersson & J.M. Smith (2000):
Martin-Löf's type theory.
In: S. Abramsky, D.M. Gabbay & T.S.E. Maibaum: Handbook of Logic in Computer Science.
Clarendon Press,
pp. 1–37.
L.C. Pereira (2017).
Personal communication.
D. Prawitz (2015):
Classical versus intuitionistic logic.
In: E.H. Haeusler, W. de Campos Sanz & B. Lopes: Why is this a Proof?, Festschrift for Luiz Carlos Pereira.
College Publications.
R. Saillard (2015):
Type Checking in the Lambda-Pi-Calculus Modulo: Theory and Practice.
École des Mines.
S.G. Simpson (2009):
Subsystems of second-order arithmetic.
Cambridge University Press,
doi:10.1017/CBO9780511581007.
F. Thiré (2017).
Personal communication.
F. Thiré (2017):
Sharing Arithmetic Proofs from Dedukti to HOL.
Manuscript.
T. Zimmermann & H. Herbelin (2015):
Automatic and Transparent Transfer of Theorems along Isomorphisms in the Coq Proof Assistant.
Work in progress session, Conference on Intelligent Computer Mathematics, https://hal.archives-ouvertes.fr/hal-01152588/file/paper.pdf.
eptcs@eptcs.org