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