References

  1. Peter B. Andrews (1986): An introduction to mathematical logic and type theory - to truth through proof. Computer science and applied mathematics. Academic Press.
  2. 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.
  3. 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.
  4. 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.
  5. 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.
  6. 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.
  7. 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.
  8. 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.
  9. 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.
  10. F. Pfenning & C. Elliott (1988): Higher-order Abstract Syntax. SIGPLAN Not. 23(7), pp. 199–208. Available at http://doi.acm.org/10.1145/960116.54010.
  11. 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.
  12. 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.
  13. The Coq Development Team (2017): The Coq Proof Assistant, version 8.7.1. Available at https://doi.org/10.5281/zenodo.1133970.
  14. The Matita development team (2018): Arithmetic library. Available at https://github.com/LPCIC/matita/tree/master/matita/matita/lib/arithmetics.
  15. 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.
  16. 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.

Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org