References

  1. Peter B. Andrews (1986): An introduction to mathematical logic and type theory: to truth through proof. Academic Press Professional, Inc., San Diego, CA, USA.
  2. Andrew W. Appel (2001): Foundational Proof-Carrying Code. In: LICS. IEEE Computer Society, Washington, DC, USA, pp. 247256, doi:10.1109/LICS.2001.932501.
  3. Ali Assaf (2015): Conservativity of embeddings in the lambda-Pi calculus modulo rewriting. Available at https://hal.archives-ouvertes.fr/hal-01084165. To appear in TLCA 2015.
  4. Ali Assaf & Raphaël Cauderlier (2015): Mixing HOL and Coq in Dedukti (Rough Diamond). Available at https://hal.inria.fr/hal-01141789. To appear in PxTP 2015.
  5. H. P. Barendregt (1992): Lambda Calculi with Types, Handbook of Logic in Computer Science Vol. II. Oxford University Press.
  6. Michael Beeson (1985): Foundations of Constructive Mathematics. Springer-Verlag, doi:10.1007/978-3-642-68952-9.
  7. M. Boespflug & G. Burel (2012): CoqInE: Translating the calculus of inductive constructions into the lambda-Pi-calculus modulo. In: PxTP, pp. 44–50.
  8. M. Boespflug, Q. Carbonneaux & O. Hermant (2012): The lambda-Pi-calculus modulo as a universal proof language. In: PxTP, pp. 28–43.
  9. Zakaria Chihani, Dale Miller & Fabien Renaud (2013): Foundational proof certificates in first-order Logic. In: Maria Paola Bonacina: Automated Deduction CADE-24, Lecture Notes in Computer Science 7898. Springer Berlin Heidelberg, pp. 162–177, doi:10.1007/978-3-642-38574-2_11.
  10. Alonzo Church (1940): A formulation of the simple theory of types. Journal of Symbolic Logic 5(02), pp. 56–68, doi:10.2307/2266170.
  11. Denis Cousineau & Gilles Dowek (2007): Embedding Pure Type Systems in the Lambda-Pi-Calculus Modulo. In: Simona Ronchi Della Rocca: TLCA, LNCS 4583. Springer Berlin Heidelberg, pp. 102–117, doi:10.1007/978-3-540-73228-0_9.
  12. Gilles Dowek (2014): Models and termination of proof-reduction in the λΠ-calculus modulo theory. Available at https://who.rocq.inria.fr/Gilles.Dowek/Publi/superpi.pdf.
  13. Herman Geuvers (1993): Logics and type systems. PhD thesis. University of Nijmegen.
  14. Herman Geuvers & Erik Barendsen (1999): Some logical and syntactical observations concerning the first-order dependent type system lambda-P. Mathematical Structures in Computer Science 9(04), pp. 335–359, doi:10.1017/S0960129599002856.
  15. Thomas C. Hales (2007): The Jordan Curve Theorem, Formally and Informally. American Mathematical Monthly 114(10), pp. 882–894.
  16. Thomas C. Hales, John Harrison, Sean McLaughlin, Tobias Nipkow, Steven Obua & Roland Zumkeller (2011): A Revision of the Proof of the Kepler Conjecture. In: Jeffrey C. Lagarias: The Kepler Conjecture. Springer New York, pp. 341–376, doi:10.1007/978-1-4614-1129-1_9.
  17. Robert Harper, Furio Honsell & Gordon Plotkin (1993): A framework for defining logics. J. ACM 40(1), pp. 143184, doi:10.1145/138027.138060.
  18. 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.
  19. Cezary Kaliszyk & Alexander Krauss (2013): Scalable LCF-Style Proof Translation. In: Sandrine Blazy, Christine Paulin-Mohring & David Pichardie: ITP, LNCS 7998. Springer Berlin Heidelberg, pp. 51–66, doi:10.1007/978-3-642-39634-2_7.
  20. 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.
  21. Dale Miller (1991): Unification of simply typed lambda-terms as logic programming. Technical Reports (CIS).
  22. Dale A. Miller (2004): Proofs in higher-order logic. University of Pennsylvania.
  23. Pavel Naumov, Mark-Oliver Stehr & José Meseguer (2001): The HOL/NuPRL Proof Translator. In: Richard J. Boulton & Paul B. Jackson: TPHOLs, LNCS 2152. Springer Berlin Heidelberg, pp. 329–345, doi:10.1007/3-540-44755-5_23.
  24. 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.
  25. Frank Pfenning & Carsten Schürmann (1999): System Description: Twelf A Meta-Logical Framework for Deductive Systems. In: CADE-16, LNCS 1632. Springer Berlin Heidelberg, pp. 202–206, doi:10.1007/3-540-48660-7_14.
  26. Florian Rabe (2010): Representing Isabelle in LF. EPTCS 34, pp. 85–99, doi:10.4204/EPTCS.34.8. arXiv: 1009.2794.
  27. Florian Rabe & Michael Kohlhase (2013): A scalable module system. Inf. Comput. 230, pp. 1–54, doi:10.1016/j.ic.2013.06.001.
  28. 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: LPAR, LNCS 4246. Springer Berlin Heidelberg, pp. 150–166, doi:10.1007/11916277_11.
  29. Freek Wiedijk (2007): The QED manifesto revisited. Studies in Logic, Grammar and Rhetoric 10(23), pp. 121–133.
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org