Document Open Access Logo

Encoding of Predicate Subtyping with Proof Irrelevance in the λΠ-Calculus Modulo Theory

Authors Gabriel Hondet, Frédéric Blanqui

PDF
Thumbnail PDF

File

LIPIcs.TYPES.2020.6.pdf
  • Filesize: 0.9 MB
  • 18 pages

Document Identifiers

Author Details

Gabriel Hondet
  • Université Paris-Saclay, ENS Paris-Saclay, CNRS, Inria, Laboratoire Méthodes Formelles, Gif-sur-Yvette, France
Frédéric Blanqui
  • Université Paris-Saclay, ENS Paris-Saclay, CNRS, Inria, Laboratoire Méthodes Formelles, Gif-sur-Yvette, France

Acknowledgements

The authors thank Gilles Dowek and the anonymous referees very much for their remarks.

Cite AsGet BibTex

Gabriel Hondet and Frédéric Blanqui. Encoding of Predicate Subtyping with Proof Irrelevance in the λΠ-Calculus Modulo Theory. In 26th International Conference on Types for Proofs and Programs (TYPES 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 188, pp. 6:1-6:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.TYPES.2020.6

Abstract

The λΠ-calculus modulo theory is a logical framework in which various logics and type systems can be encoded, thus helping the cross-verification and interoperability of proof systems based on those logics and type systems. In this paper, we show how to encode predicate subtyping and proof irrelevance, two important features of the PVS proof assistant. We prove that this encoding is correct and that encoded proofs can be mechanically checked by Dedukti, a type checker for the λΠ-calculus modulo theory using rewriting.

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
  • Theory of computation → Higher order logic
  • Theory of computation → Equational logic and rewriting
Keywords
  • Predicate Subtyping
  • Logical Framework
  • PVS
  • Dedukti
  • Proof Irrelevance

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Andreas Abel, Thierry Coquand, and Miguel Pagano. A modular type-checking algorithm for type theory with singleton types and proof irrelevance. Log. Methods Comput. Sci., 7(2), 2011. URL: https://doi.org/10.2168/LMCS-7(2:4)2011.
  2. Andrea Asperti, Wilmer Ricciotti, and Claudio Sacerdoti Coen. Matita tutorial. J. Formaliz. Reason., 7(2):91-199, 2014. URL: https://doi.org/10.6092/issn.1972-5787/4651.
  3. A. Assaf. A framework for defining computational higher-order logics. PhD thesis, École Polytechnique, France, 2015. URL: https://tel.archives-ouvertes.fr/tel-01235303/.
  4. A. Assaf, G. Burel, R. Cauderlier, D. Delahaye, G. Dowek, C. Dubois, F. Gilbert, P. Halmagrand, O. Hermant, and R. Saillard. Dedukti: a logical framework based on the λπ-calculus modulo theory, 2019. Draft. URL: http://lsv.fr/~dowek/Publi/expressing.pdf.
  5. Ali Assaf and Guillaume Burel. Translating HOL to dedukti. In Cezary Kaliszyk and Andrei Paskevich, editors, Proceedings Fourth Workshop on Proof eXchange for Theorem Proving, PxTP 2015, Berlin, Germany, August 2-3, 2015, volume 186 of EPTCS, pages 74-88, 2015. URL: https://doi.org/10.4204/EPTCS.186.8.
  6. Franz Baader and Tobias Nipkow. Term rewriting and all that. Cambridge University Press, 1998. Google Scholar
  7. Henk Barendregt and Kees Hemerik. Types in Lambda Calculi and Programming Languages. In Neil D. Jones, editor, ESOP'90, 3rd European Symposium on Programming, Copenhagen, Denmark, May 15-18, 1990, Proceedings, volume 432 of Lecture Notes in Computer Science, pages 1-35. Springer, 1990. URL: https://doi.org/10.1007/3-540-52592-0_53.
  8. F. Blanqui. Théorie des types et récriture. PhD thesis, Université Paris-Sud, France, 2001. URL: http://tel.archives-ouvertes.fr/tel-00105522.
  9. Frédéric Blanqui. Definitions by rewriting in the calculus of constructions. Mathematical Structures in Computer Science, 15(1), 2005. URL: https://doi.org/10.1017/S0960129504004426.
  10. M. Boespflug and G. Burel. CoqInE: translating the calculus of inductive constructions into the lambda-Pi-calculus modulo. In Proceedings of the 2nd International Workshop on Proof eXchange for Theorem Proving, CEUR Workshop Proceedings 878, 2012. URL: http://ceur-ws.org/Vol-878/paper3.pdf.
  11. Robert L. Constable, Stuart F. Allen, Mark Bromley, Rance Cleaveland, J. F. Cremer, R. W. Harper, Douglas J. Howe, Todd B. Knoblock, N. P. Mendler, Prakash Panangaden, James T. Sasaki, and Scott F. Smith. Implementing mathematics with the Nuprl proof development system. Prentice Hall, 1986. URL: http://dl.acm.org/citation.cfm?id=10510.
  12. D. Cousineau and G. Dowek. Embedding pure type systems in the lambda-Pi-calculus modulo. In Proceedings of the 8th International Conference on Typed Lambda Calculi and Applications, Lecture Notes in Computer Science 4583, 2007. URL: https://doi.org/10.1007/978-3-540-73228-0_9.
  13. N.G. de Bruijn. Some Extensions of Automath: The AUT-4 Family. In R.P. Nederpelt, J.H. Geuvers, and R.C. de Vrijer, editors, Selected Papers on Automath, volume 133 of Studies in Logic and the Foundations of Mathematics, pages 283-288. Elsevier, 1994. URL: https://doi.org/10.1016/S0049-237X(08)70209-X.
  14. Leonardo Mendonça de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer. The lean theorem prover (system description). In Amy P. Felty and Aart Middeldorp, editors, Automated Deduction - CADE-25 - 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings, volume 9195 of Lecture Notes in Computer Science, pages 378-388. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-21401-6_26.
  15. Gilles Dowek. Models and termination of proof reduction in the lambda pi-calculus modulo theory. In Ioannis Chatzigiannakis, Piotr Indyk, Fabian Kuhn, and Anca Muscholl, editors, 44th International Colloquium on Automata, Languages, and Programming, ICALP 2017, July 10-14, 2017, Warsaw, Poland, volume 80 of LIPIcs, pages 109:1-109:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. URL: https://doi.org/10.4230/LIPIcs.ICALP.2017.109.
  16. G. Genestier. ncoding agda programs using rewriting. In Proceedings of the 5th International Conference on Formal Structures for Computation and Deduction, Leibniz International Proceedings in Informatics 167, 2020. URL: https://doi.org/10.4230/LIPIcs.FSCD.2020.31.
  17. Frederic Gilbert. Extending higher-order logic with predicate subtyping : application to PVS. Theses, Université Sorbonne Paris Cité, 2018. URL: https://tel.archives-ouvertes.fr/tel-02058937.
  18. Gaëtan Gilbert, Jesper Cockx, Matthieu Sozeau, and Nicolas Tabareau. Definitional proof-irrelevance without k. Proc. ACM Program. Lang., 3(POPL), 2019. URL: https://doi.org/10.1145/3290316.
  19. Mohamed Yacine El Haddad, Guillaume Burel, and Frédéric Blanqui. EKSTRAKTO A tool to reconstruct dedukti proofs from TSTP files (extended abstract). In Giselle Reis and Haniel Barbosa, editors, Proceedings Sixth Workshop on Proof eXchange for Theorem Proving, PxTP 2019, Natal, Brazil, August 26, 2019, volume 301 of EPTCS, pages 27-35, 2019. URL: https://doi.org/10.4204/EPTCS.301.5.
  20. Joe Hurd. Predicate subtyping with predicate sets. In Richard J. Boulton and Paul B. Jackson, editors, Theorem Proving in Higher Order Logics, 14th International Conference, TPHOLs 2001, Edinburgh, Scotland, UK, September 3-6, 2001, Proceedings, volume 2152 of Lecture Notes in Computer Science, pages 265-280. Springer, 2001. URL: https://doi.org/10.1007/3-540-44755-5_19.
  21. Matt Kaufmann and J. Strother Moore. An industrial strength theorem prover for a logic based on common lisp. IEEE Trans. Software Eng., 23(4):203-213, 1997. URL: https://doi.org/10.1109/32.588534.
  22. Jan Willem Klop, Vincent van Oostrom, and Femke van Raamsdonk. Combinatory reduction systems: Introduction and survey. Theor. Comput. Sci., 121(1&2):279-308, 1993. URL: https://doi.org/10.1016/0304-3975(93)90091-7.
  23. D. Knuth and P. Bendix. Simple word problems in universal algebras. In Automation of Reasoning. Symbolic Computation (Artificial Intelligence). Springer, 1983. Google Scholar
  24. William Lovas and Frank Pfenning. Refinement types for logical frameworks and their interpretation as proof irrelevance. Log. Methods Comput. Sci., 6(4), 2010. URL: https://doi.org/10.2168/LMCS-6(4:5)2010.
  25. Zhaohui Luo. An extended calculus of constructions. PhD thesis, University of Edinburgh, UK, 1990. URL: http://hdl.handle.net/1842/12487.
  26. S. Owre, N. Shankar, J. M. Rushby, and D. W. J. Stringer-Calvert. PVS Language Reference. Computer Science Laboratory, SRI International, Menlo Park, CA, 1999. Google Scholar
  27. Sam Owre, John Rushby, N. Shankar, and David Stringer-Calvert. PVS: an experience report. In Dieter Hutter, Werner Stephan, Paolo Traverso, and Markus Ullman, editors, Applied Formal Methods - FM-Trends 98, volume 1641 of Lecture Notes in Computer Science, pages 338-345, Boppard, Germany, October 1998. Springer-Verlag. URL: http://www.csl.sri.com/papers/fmtrends98/.
  28. Sam Owre and Natarajan Shankar. The formal semantics of PVS. Technical Report SRI-CSL-97-2, Computer Science Laboratory, SRI International, Menlo Park, CA, 1997. Google Scholar
  29. Frank Pfenning. Intensionality, extensionality, and proof irrelevance in modal type theory. In 16th Annual IEEE Symposium on Logic in Computer Science, Boston, Massachusetts, USA, June 16-19, 2001, Proceedings, pages 221-230. IEEE Computer Society, 2001. URL: https://doi.org/10.1109/LICS.2001.932499.
  30. John M. Rushby, Sam Owre, and Natarajan Shankar. Subtypes for specifications: Predicate subtyping in PVS. IEEE Trans. Software Eng., 24(9):709-720, 1998. URL: https://doi.org/10.1109/32.713327.
  31. Anne Salvesen and Jan M. Smith. The strength of the subset type in martin-löf’s type theory. In Proceedings of the Third Annual Symposium on Logic in Computer Science (LICS '88), Edinburgh, Scotland, UK, July 5-8, 1988, pages 384-391. IEEE Computer Society, 1988. URL: https://doi.org/10.1109/LICS.1988.5135.
  32. Matthieu Sozeau. Subset coercions in coq. In Thorsten Altenkirch and Conor McBride, editors, Types for Proofs and Programs, International Workshop, TYPES 2006, Nottingham, UK, April 18-21, 2006, Revised Selected Papers, volume 4502 of Lecture Notes in Computer Science, pages 237-252. Springer, 2006. URL: https://doi.org/10.1007/978-3-540-74464-1_16.
  33. The Agda Team. Agda Manual. URL: https://agda.readthedocs.io/.
  34. F. Thiré. Interoperability between proof systems using the Dedukti logical framework. PhD thesis, Université Paris-Saclay, France, 2020. Google Scholar
  35. F. Thiré and G. Férey. Proof irrelevance and predicate subtyping in dedukti. https://eutypes.cs.ru.nl/eutypes_pmwiki/uploads/Main/books-of-abstracts-TYPES2019.pdf, p. 106, 2019. Abstract of a talk given at the TYPES conference.
  36. Benjamin Werner. On the strength of proof-irrelevant type theories. Log. Methods Comput. Sci., 4(3), 2008. URL: https://doi.org/10.2168/LMCS-4(3:13)2008.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact