Ali Assaf (2014):
A calculus of constructions with explicit subtyping.
Available at https://hal.inria.fr/hal-01097401.
Accepted in Postproceedings of Types 2014.
Ali Assaf (2015):
Conservativity of embeddings in the lambda-Pi calculus modulo rewriting.
In: Thorsten Altenkirch: International Conference on Typed Lambda Calculi and Applications (TLCA),
LIPIcs 38.
Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik,
pp. 31–44,
doi:10.4230/LIPIcs.TLCA.2015.31.
Ali Assaf & Guillaume Burel (2015):
Translating HOL to Dedukti.
Available at https://hal.inria.fr/hal-01097412.
Accepted in PxTP 2015.
Henk Barendregt (1992):
Lambda calculi with types.
In: Samson Abramsky, Dov M. Gabbay & Thomas S. E. Maibaum: Handbook of Logic in Computer Science 2.
Oxford University Press,
pp. 117–309.
M. Boespflug, Q. Carbonneaux & O. Hermant (2012):
The lambda-Pi-calculus modulo as a universal proof language.
In: Proof Exchange for Theorem Proving - Second International Workshop, PxTP 2012,
pp. 28–43.
Mathieu Boespflug & Guillaume Burel (2012):
CoqInE: Translating the calculus of inductive constructions into the λΠ-calculus modulo.
In: Proof Exchange for Theorem Proving - Second International Workshop, PxTP 2012,
pp. 44.
Richard Bonichon, David Delahaye & Damien Doligez (2007):
Zenon: An Extensible Automated Theorem Prover Producing Checkable Proofs.
In: Logic for Programming Artificial Intelligence and Reasoning (LPAR),
LNCS/LNAI 4790.
Springer,
pp. 151–165,
doi:10.1007/978-3-540-75560-9_13.
Guillaume Burel (2013):
A Shallow Embedding of Resolution and Superposition Proofs into the λΠ-Calculus Modulo.
In: Jasmin Christian Blanchette & Josef Urban: Proof Exchange for Theorem Proving - Third International Workshop, PxTP 2013,
EPiC 14.
EasyChair,
pp. 43–57.
Raphaël Cauderlier & Pierre Halmagrand (2015):
Checking Zenon Modulo proofs in Dedukti.
Accepted in PxTP 2015.
Denis Cousineau & Gilles Dowek (2007):
Embedding Pure Type Systems in the Lambda-Pi-Calculus Modulo.
In: Simona Ronchi Della Rocca: Typed Lambda Calculi and Applications, 8th International Conference, TLCA 2007, Paris, France, June 26-28, 2007, Proceedings,
LNCS 4583.
Springer,
pp. 102–117,
doi:10.1007/978-3-540-73228-0_9.
David Delahaye, Damien Doligez, Frédéric Gilbert, Pierre Halmagrand & Olivier Hermant (2013):
Zenon Modulo: When Achilles Outruns the Tortoise Using Deduction Modulo.
In: Ken McMillan, Aart Middeldorp & Andrei Voronkov: LPAR,
LNCS 8312.
Springer Berlin Heidelberg,
pp. 274–290,
doi:10.1007/978-3-642-45221-5_20.
Herman Geuvers (1993):
Logics and type systems.
PhD thesis.
University of Nijmegen.
Robert Harper, Furio Honsell & Gordon Plotkin (1993):
A framework for defining logics.
Journal of the ACM 40(1),
pp. 143–184,
doi:10.1145/138027.138060.
John Harrison (2009):
HOL Light: An Overview.
In: Stefan Berghofer, Tobias Nipkow, Christian Urban & Makarius Wenzel: Theorem Proving in Higher Order Logics,
LNCS 5674.
Springer Berlin Heidelberg,
pp. 60–66,
doi:10.1007/978-3-642-03359-9_4.
Fulya Horozal & Florian Rabe (2011):
Representing model theory in a type-theoretical logical framework.
Theoretical Computer Science 412,
pp. 4919–4945,
doi:10.1016/j.tcs.2011.03.022.
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: Interactive Theorem Proving,
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.
Pavel Naumov, Mark-Oliver Stehr & José Meseguer (2001):
The HOL/NuPRL proof translator.
In: Richard J. Boulton & Paul B. Jackson: Theorem Proving in Higher Order Logics,
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: Automated Deduction CADE-16,
LNCS 1632.
Springer Berlin Heidelberg,
pp. 202–206,
doi:10.1007/3-540-48660-7_14.
Ronan Saillard (2013):
Dedukti: a universal proof checker.
In: Foundation of Mathematics for Computer-Aided Formalization Workshop,
Padova.
Available at https://hal.inria.fr/hal-00833992.
Ronan Saillard (2013):
Towards explicit rewrite rules in the λΠ-calculus modulo.
In: IWIL - 10th International Workshop on the Implementation of Logics.
Available at https://hal.inria.fr/hal-00921340.
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: Logic for Programming, Artificial Intelligence, and Reasoning,
LNCS 4246.
Springer Berlin Heidelberg,
pp. 150–166,
doi:10.1007/11916277_11.
Geoff Sutcliffe, Stephan Schulz, Koen Claessen & Allen Van Gelder (2006):
Using the TPTP Language for Writing Derivations and Finite Interpretations.
In: Ulrich Furbach & Natarajan Shankar: Automated Reasoning,
LNCS 4130.
Springer Berlin Heidelberg,
pp. 67–81,
doi:10.1007/11814771_7.
The Coq development team (2012):
The Coq Reference Manual, version 8.4.
Available at http://coq.inria.fr/doc.
eptcs@eptcs.org