Document Open Access Logo

Impredicativity, Cumulativity and Product Covariance in the Logical Framework Dedukti

Authors Thiago Felicissimo, Théo Winterhalter

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2024.21.pdf
  • Filesize: 0.94 MB
  • 23 pages

Document Identifiers

Author Details

Thiago Felicissimo
  • Université Paris-Saclay, INRIA project Deducteam, Laboratoire Méthodes Formelles, ENS Paris-Saclay, France
Théo Winterhalter
  • Université Paris-Saclay, INRIA project Deducteam, Laboratoire Méthodes Formelles, ENS Paris-Saclay, France

Acknowledgements

The authors thank François Thiré and Yoan Géran for helpful remarks about a first draft, Gaspard Férey, Jean-Pierre Jouannaud, Frédéric Blanqui and Gilles Dowek for informative discussions around the subject of this paper, and the anonymous reviewers for their helpful comments.

Cite AsGet BibTex

Thiago Felicissimo and Théo Winterhalter. Impredicativity, Cumulativity and Product Covariance in the Logical Framework Dedukti. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 21:1-21:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.FSCD.2024.21

Abstract

Proof assistants such as Coq implement a type theory featuring three important features: impredicativity, cumulativity and product covariance. This combination has proven difficult to be expressed in the logical framework Dedukti, and previous attempts have failed in providing an encoding that is proven confluent, sound and conservative. In this work we solve this longstanding open problem by providing an encoding of these three features that we prove to be confluent, sound and to satisfy a restricted (but, we argue, strong enough) form of conservativity. Our proof of confluence is a contribution by itself, and combines various criteria and proof techniques from rewriting theory. Our proof of soundness also contributes a new strategy in which the result is shown in terms of an inverse translation function, fixing a common flaw made in some previous encoding attempts.

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
  • Theory of computation → Equational logic and rewriting
Keywords
  • Dedukti
  • Rewriting
  • Confluence
  • Dependent types
  • Cumulativity
  • Universes

Metrics

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

Related Versions

Supplementary Materials

References

  1. AProVE. URL: https://aprove.informatik.rwth-aachen.de/.
  2. CeTA. URL: http://cl-informatik.uibk.ac.at/software/ceta/.
  3. CSIho. URL: http://cl-informatik.uibk.ac.at/software/csi/ho/.
  4. Ali Assaf. A calculus of constructions with explicit subtyping. In 20th International Conference on Types for Proofs and Programs (TYPES 2014), volume 39, 2014. Google Scholar
  5. Ali Assaf. A framework for defining computational higher-order logics. These, École polytechnique, September 2015. URL: https://pastel.archives-ouvertes.fr/tel-01235303.
  6. Ali Assaf. Conservativity of Embeddings in the lambda Pi Calculus Modulo Rewriting. In Thorsten Altenkirch, editor, 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015), volume 38 of Leibniz International Proceedings in Informatics (LIPIcs), pages 31-44, Dagstuhl, Germany, 2015. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.TLCA.2015.31.
  7. Ali Assaf, Guillaume Burel, Raphaël Cauderlier, David Delahaye, Gilles Dowek, Catherine Dubois, Frédéric Gilbert, Pierre Halmagrand, Olivier Hermant, and Ronan Saillard. Dedukti: a logical framework based on the λΠ-calculus modulo theory. Unpublished, 2016. Google Scholar
  8. Ali Assaf, Gilles Dowek, Jean-Pierre Jouannaud, and Jiaxiang Liu. Untyped Confluence In Dependent Type Theories. working paper or preprint, April 2017. URL: https://hal.inria.fr/hal-01515505.
  9. H.P. Barendregt. The Lambda Calculus: Its Syntax and Semantics. Studies in Logic and the Foundations of Mathematics. Elsevier Science, 1984. Google Scholar
  10. Bruno Barras. Auto-validation d’un systeme de preuves avec familles inductives. These de doctorat, Université Paris, 7, 1999. Google Scholar
  11. M. Bezem, J.W. Klop, R. de Vrijer, and Terese. Term Rewriting Systems. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2003. URL: https://books.google.fr/books?id=7QQ5u-4tRUkC.
  12. Frédéric Blanqui. Théorie des types et réécriture. (Type theory and rewriting). PhD thesis, University of Paris-Sud, Orsay, France, 2001. URL: https://tel.archives-ouvertes.fr/tel-00105522.
  13. Frédéric Blanqui. Type safety of rewrite rules in dependent types. In 5th International Conference on Formal Structures for Computation and Deduction, 2020. Google Scholar
  14. Frédéric Blanqui. Encoding type universes without using matching modulo AC. In Proceedings of the 7th International Conference on Formal Structures for Computation and Deduction, Leibniz International Proceedings in Informatics 228, 2022. URL: https://doi.org/10.4230/LIPIcs.FSCD.2022.24.
  15. Frédéric Blanqui. HOL-Light library in Coq. URL: https://github.com/Deducteam/coq-hol-light.
  16. Frédéric Blanqui, Gilles Dowek, Emilie Grienenberger, Gabriel Hondet, and François Thiré. A modular construction of type theories. Logical Methods in Computer Science, Volume 19, Issue 1, February 2023. URL: https://doi.org/10.46298/lmcs-19(1:12)2023.
  17. Valentin Blot, Gilles Dowek, and Thomas Traversié. An Implementation of Set Theory with Pointed Graphs in Dedukti. In LFMTP 2022 - International Workshop on Logical Frameworks and Meta-Languages : Theory and Practice, Haïfa, Israel, August 2022. URL: https://inria.hal.science/hal-03740004.
  18. Denis Cousineau and Gilles Dowek. Embedding pure type systems in the lambda-pi-calculus modulo. In Simona Ronchi Della Rocca, editor, Typed Lambda Calculi and Applications, pages 102-117, Berlin, Heidelberg, 2007. Springer Berlin Heidelberg. Google Scholar
  19. Deducteam. An encoding of impredicativity, cumulativity and product covariance in the logical framework dedukti. URL: https://github.com/Deducteam/cc-in-dk.
  20. Deducteam. Pull request for ACU matching in DkCheck. URL: https://github.com/Deducteam/Dedukti/pull/219.
  21. Gilles Dowek, Gaspard Férey, Jean-Pierre Jouannaud, and Jiaxiang Liu. Confluence of left-linear higher-order rewrite theories by checking their nested critical pairs. Mathematical Structures in Computer Science, 32(7):898-933, 2022. URL: https://doi.org/10.1017/S0960129522000044.
  22. Thiago Felicissimo. Adequate and Computational Encodings in the Logical Framework Dedukti. In Amy P. Felty, editor, 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022), volume 228 of Leibniz International Proceedings in Informatics (LIPIcs), pages 25:1-25:18, Dagstuhl, Germany, 2022. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.FSCD.2022.25.
  23. Thiago Felicissimo. Generic bidirectional typing for dependent type theories. In Stephanie Weirich, editor, Programming Languages and Systems, pages 143-170, Cham, 2024. Springer Nature Switzerland. Google Scholar
  24. Thiago Felicissimo, Frédéric Blanqui, and Ashish Kumar Barnawal. Translating Proofs from an Impredicative Type System to a Predicative One. In Bartek Klin and Elaine Pimentel, editors, 31st EACSL Annual Conference on Computer Science Logic (CSL 2023), volume 252 of Leibniz International Proceedings in Informatics (LIPIcs), pages 19:1-19:19, Dagstuhl, Germany, 2023. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.CSL.2023.19.
  25. Gaspard Férey and Jean-Pierre Jouannaud. Confluence in non-left-linear untyped higher-order rewrite theories. In Proceedings of the 23rd International Symposium on Principles and Practice of Declarative Programming, PPDP '21, New York, NY, USA, 2021. Association for Computing Machinery. URL: https://doi.org/10.1145/3479394.3479403.
  26. Gaspard Férey. Higher-Order Confluence and Universe Embedding in the Logical Framework. These, Université Paris-Saclay, June 2021. URL: https://tel.archives-ouvertes.fr/tel-03418761.
  27. Jan Herman Geuvers. Logics and type systems. [Sl: sn], 1993. Google Scholar
  28. Jürgen Giesl, René Thiemann, Peter Schneider-Kamp, and Stephan Falke. Automated termination proofs with AProVE. In Rewriting Techniques and Applications: 15th International Conference, RTA 2004, Aachen, Germany, June 3-5, 2004. Proceedings 15, pages 210-220. Springer, 2004. Google Scholar
  29. Yoan Géran. Mathématiques inversées de Coq, 2021. URL: https://inria.hal.science/hal-04319183.
  30. Makoto Hamana. How to prove your calculus is decidable: Practical applications of second-order algebraic theories and computation. Proc. ACM Program. Lang., 1(ICFP), August 2017. URL: https://doi.org/10.1145/3110266.
  31. Hugo Herbelin. Type inference with algebraic universes in the calculus of inductive constructions. Unpublished. Available at: pauillac. inria. fr/ herbelin/publis/univalgcci. pdf, 2005. Google Scholar
  32. Gabriel Hondet and Frédéric Blanqui. Encoding of Predicate Subtyping with Proof Irrelevance in the Lambdapi-Calculus Modulo Theory. In Ugo de'Liguoro, Stefano Berardi, and Thorsten Altenkirch, editors, 26th International Conference on Types for Proofs and Programs (TYPES 2020), volume 188 of Leibniz International Proceedings in Informatics (LIPIcs), pages 6:1-6:18, Dagstuhl, Germany, 2021. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.TYPES.2020.6.
  33. Jan Willem Klop. Combinatory reduction systems. PhD thesis, Rijksuniversiteit Utrecht, 1963. Google Scholar
  34. Marc Lasson. Réalisabilité et paramétricité dans les systèmes de types purs. Theses, Ecole normale supérieure de lyon - ENS LYON, November 2012. URL: https://theses.hal.science/tel-00770669.
  35. Zhaohui Luo. An extended calculus of constructions. PhD thesis, University of Edinburgh, 1990. Google Scholar
  36. Richard Mayr and Tobias Nipkow. Higher-order rewrite systems and their confluence. Theoretical computer science, 192(1):3-29, 1998. Google Scholar
  37. Dale Miller. A logic programming language with lambda-abstraction, function variables, and simple unification. Journal of logic and computation, 1(4):497-536, 1991. Google Scholar
  38. Julian Nagele, Bertram Felgenhauer, and Aart Middeldorp. CSI: New evidence - a progress report. In Leonardo de Moura, editor, Proceedings of the 26th International Conference on Automated Deduction (CADE-26), volume 10395 of Lecture Notes in Artificial Intelligence, pages 385-397, 2017. URL: https://doi.org/10.1007/978-3-319-63046-5_24.
  39. Nicolas Oury. Extensionality in the calculus of constructions. In Theorem Proving in Higher Order Logics: 18th International Conference, TPHOLs 2005, Oxford, UK, August 22-25, 2005. Proceedings 18, pages 278-293. Springer, 2005. Google Scholar
  40. Ronan Saillard. Rewriting modulo β in the λπ-calculus modulo. Electronic Proceedings in Theoretical Computer Science, 185:87-101, July 2015. URL: https://doi.org/10.4204/eptcs.185.6.
  41. Ronan Saillard. Type checking in the Lambda-Pi-calculus modulo: theory and practice. PhD thesis, Mines ParisTech, France, 2015. URL: https://pastel.archives-ouvertes.fr/tel-01299180.
  42. The Coq Development Team. Typing rules for Coq. URL: https://coq.inria.fr/doc/V8.16.1/refman/language/cic.html#id6.
  43. René Thiemann and Christian Sternagel. Certification of termination proofs using ceta. In International Conference on Theorem Proving in Higher Order Logics, pages 452-468. Springer, 2009. Google Scholar
  44. François Thiré. Sharing a library between proof assistants: Reaching out to the HOL family. In Frédéric Blanqui and Giselle Reis, editors, Proceedings of the 13th International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP@FSCD 2018, Oxford, UK, 7th July 2018, volume 274 of EPTCS, pages 57-71, 2018. URL: https://doi.org/10.4204/EPTCS.274.5.
  45. François Thiré. Interoperability between proof systems using the logical framework Dedukti. PhD thesis, ENS Paris-Saclay, 2020. Google Scholar
  46. Vincent van Oostrom. Developing developments. Theoretical Computer Science, 175(1):159-181, 1997. Google Scholar
  47. Vincent van Oostrom and Femke van Raamsdonk. Weak orthogonality implies confluence: The higher-order case. In Gerhard Goos, Juris Hartmanis, Anil Nerode, and Yu. V. Matiyasevich, editors, Logical Foundations of Computer Science, volume 813, pages 379-392. Springer Berlin Heidelberg, Berlin, Heidelberg, 1994. Series Title: Lecture Notes in Computer Science. URL: https://doi.org/10.1007/3-540-58140-5_35.
  48. Théo Winterhalter, Matthieu Sozeau, and Nicolas Tabareau. Eliminating Reflection from Type Theory. In CPP 2019 - 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, pages 91-103, Lisbonne, Portugal, January 2019. ACM. URL: https://doi.org/10.1145/3293880.3294095.
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