Peter B. Andrews (1986):
An introduction to mathematical logic and type theory - to truth through proof.
Computer science and applied mathematics.
Academic Press.
Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen & Enrico Tassi (2011):
The Matita Interactive Theorem Prover.
In: Nikolaj Bjørner & Viorica Sofronie-Stokkermans: Automated Deduction - CADE-23 - 23rd International Conference on Automated Deduction, Wroclaw, Poland, July 31 - August 5, 2011. Proceedings,
Lecture Notes in Computer Science 6803.
Springer,
pp. 64–69.
Available at https://doi.org/10.1007/978-3-642-22438-6_7.
Raphaël Cauderlier & Catherine Dubois (2017):
FoCaLiZe and Dedukti to the Rescue for Proof Interoperability.
In: Mauricio Ayala-Rincón & César A. Muñoz: Interactive Theorem Proving - 8th International Conference, ITP 2017, Brasília, Brazil, September 26-29, 2017, Proceedings,
Lecture Notes in Computer Science 10499.
Springer,
pp. 131–147.
Available at https://doi.org/10.1007/978-3-319-66107-0_9.
Zakaria Chihani, Dale Miller & Fabien Renaud (2013):
Foundational Proof Certificates in First-Order Logic.
In: Maria Paola Bonacina: Automated Deduction - CADE-24 - 24th International Conference on Automated Deduction, Lake Placid, NY, USA, June 9-14, 2013. Proceedings,
Lecture Notes in Computer Science 7898.
Springer,
pp. 162–177.
Available at https://doi.org/10.1007/978-3-642-38574-2_11.
Thierry Coquand (1986):
An Analysis of Girard's Paradox.
In: Proceedings of the Symposium on Logic in Computer Science (LICS '86), Cambridge, Massachusetts, USA, June 16-18, 1986.
IEEE Computer Society,
pp. 227–236.
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,
Lecture Notes in Computer Science 4583.
Springer,
pp. 102–117.
Available at http://dx.doi.org/10.1007/978-3-540-73228-0_9.
Robert Harper, Furio Honsell & Gordon D. Plotkin (1993):
A Framework for Defining Logics.
J. ACM 40(1),
pp. 143–184.
Available at http://doi.acm.org/10.1145/138027.138060.
Joe Hurd (2011):
The OpenTheory Standard Theory Library.
In: Mihaela Bobaru, Klaus Havelund, Gerard J. Holzmann & Rajeev Joshi: Third International Symposium on NASA Formal Methods (NFM 2011),
Lecture Notes in Computer Science 6617.
Springer,
pp. 177–191.
Available at https://doi.org/10.1007/3-540-60275-5_76.
Chantal Keller & Benjamin Werner (2010):
Importing HOL Light into Coq.
In: Matt Kaufmann & Lawrence C. Paulson: Interactive Theorem Proving, First International Conference, ITP 2010, Edinburgh, UK, July 11-14, 2010. Proceedings,
Lecture Notes in Computer Science 6172.
Springer,
pp. 307–322.
Available at https://doi.org/10.1007/978-3-642-14052-5_22.
Brigitte Pientka (2008):
A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions.
In: 35th Annual ACM Symposium on Principles of Programming Languages (POPL'08).
ACM,
pp. 371–382.
Available at https://doi.org/10.1145/1328438.1328483.
Ronan Saillard (2015):
Typechecking in the lambda-Pi-Calculus Modulo : Theory and Practice. (Vérification de typage pour le lambda-Pi-Calcul Modulo : théorie et pratique).
Mines ParisTech, France.
Available at https://tel.archives-ouvertes.fr/tel-01299180.
François Thiré (2018):
Interoperability in Dedukti: From the Calculus of Inductive Constructions to an extension of HOL..
http://www.lsv.fr/~fthire/research/interop/index.php.
François Thiré (2018):
Sharing a library between proof assistants: reaching out to the HOL family..
http://www.lsv.fr/~fthire/research/sttforall/index.php.