Adequate and Computational Encodings in the Logical Framework Dedukti

Author Thiago Felicissimo



PDF
Thumbnail PDF

File

LIPIcs.FSCD.2022.25.pdf
  • Filesize: 0.9 MB
  • 18 pages

Document Identifiers

Author Details

Thiago Felicissimo
  • Université Paris-Saclay, INRIA project Deducteam, Laboratoire de Méthodes Formelles, ENS Paris-Saclay, 91190, France

Acknowledgements

I would like to thank my PhD advisors Frédéric Blanqui and Gilles Dowek for the helpful discussions and comments on this paper. I would also like to thank the anonymous reviewers for their very helpful comments and suggestions.

Cite AsGet BibTex

Thiago Felicissimo. Adequate and Computational Encodings in the Logical Framework Dedukti. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 25:1-25:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.FSCD.2022.25

Abstract

Dedukti is a very expressive logical framework which unlike most frameworks, such as the Edinburgh Logical Framework (LF), allows for the representation of computation alongside deduction. However, unlike LF encodings, Dedukti encodings proposed until now do not feature an adequacy theorem - i.e., a bijection between terms in the encoded system and in its encoding. Moreover, many of them also do not have a conservativity result, which compromises the ability of Dedukti to check proofs written in such encodings. We propose a different approach for Dedukti encodings which do not only allow for simpler conservativity proofs, but which also restore the adequacy of encodings. More precisely, we propose in this work adequate (and thus conservative) encodings for Functional Pure Type Systems. However, in contrast with LF encodings, ours is computational - that is, represents computation directly as computation. Therefore, our work is the first to present and prove correct an approach allowing for encodings that are both adequate and computational in Dedukti.

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
  • Theory of computation → Equational logic and rewriting
Keywords
  • Type Theory
  • Logical Frameworks
  • Rewriting
  • Dedukti
  • Pure Type Systems

Metrics

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

References

  1. Ali Assaf. A framework for defining computational higher-order logics. Thesis, École polytechnique, September 2015. URL: https://pastel.archives-ouvertes.fr/tel-01235303.
  2. Ali Assaf. Conservativity of embeddings in the lambda pi calculus modulo rewriting. In 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015). Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2015. Google Scholar
  3. Ali Assaf, Guillaume Burel, Raphaël 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. Manuscript, 2016. Google Scholar
  4. Gilles Barthe. The relevance of proof-irrelevance. In Kim G. Larsen, Sven Skyum, and Glynn Winskel, editors, Automata, Languages and Programming, pages 755-768, Berlin, Heidelberg, 1998. Springer Berlin Heidelberg. Google Scholar
  5. Andrej Bauer, Philipp G. Haselwarter, and Peter LeFanu Lumsdaine. A general definition of dependent type theories, 2020. URL: http://arxiv.org/abs/2009.05539.
  6. 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.
  7. Frédéric Blanqui. Type safety of rewrite rules in dependent types. In FSCD 2020 - 5th International Conference on Formal Structures for Computation and Deduction, volume 167, page 14, Paris, France, June 2020. URL: https://doi.org/10.4230/LIPIcs.FSCD.2020.13.
  8. Frédéric Blanqui, Guillaume Genestier, and Olivier Hermant. Dependency pairs termination in dependent type theory modulo rewriting. In Herman Geuvers, editor, 4th International Conference on Formal Structures for Computation and Deduction, FSCD 2019, June 24-30, 2019, Dortmund, Germany, volume 131 of LIPIcs, pages 9:1-9:21. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. URL: https://doi.org/10.4230/LIPIcs.FSCD.2019.9.
  9. 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
  10. Deducteam. Lambdapi. URL: https://github.com/Deducteam/lambdapi.
  11. Gilles Dowek. Models and termination of proof reduction in the lambda pi-calculus modulo theory. In ICALP, 2017. Google Scholar
  12. Thiago Felicissimo. Adequate and computational encodings in the logical framework Dedukti. Draft at https://lmf.cnrs.fr/Perso/ThiagoFelicissimo, 2022.
  13. Thiago Felicissimo. No need to be implicit! Draft at https://lmf.cnrs.fr/Perso/ThiagoFelicissimo, 2022.
  14. Gaspard Ferey. Higher-Order Confluence and Universe Embedding in the Logical Framework. Thesis, Université Paris-Saclay, June 2021. URL: https://tel.archives-ouvertes.fr/tel-03418761.
  15. Guillaume Genestier. Dependently-Typed Termination and Embedding of Extensional Universe-Polymorphic Type Theory using Rewriting. PhD thesis, Paris-Saclay, 2020. Thèse de doctorat dirigée par Blanqui, Frédéric et Hermant, Olivier. URL: http://www.theses.fr/2020UPASG045.
  16. Robert Harper. An equational logical framework for type theories. arXiv preprint, 2021. URL: http://arxiv.org/abs/2106.01484.
  17. Robert Harper, Furio Honsell, and Gordon Plotkin. A framework for defining logics. J. ACM, 40(1):143-184, January 1993. URL: https://doi.org/10.1145/138027.138060.
  18. Gabriel Hondet and Frédéric Blanqui. Encoding of Predicate Subtyping with Proof Irrelevance in the λΠ-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.
  19. Jan Willem Klop, Vincent van Oostrom, and Femke van Raamsdonk. Combinatory reduction systems: introduction and survey. Theoretical Computer Science, 121(1):279-308, 1993. URL: https://doi.org/10.1016/0304-3975(93)90091-7.
  20. Paul-André Melliès and Benjamin Werner. A generic normalisation proof for pure type systems. In Eduardo Giménez and Christine Paulin-Mohring, editors, Types for Proofs and Programs, pages 254-276, Berlin, Heidelberg, 1998. Springer Berlin Heidelberg. Google Scholar
  21. Vincent Siles and Hugo Herbelin. Pure type system conversion is always typable. Journal of Functional Programming, 22:153-180, 2012. Google Scholar
  22. 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.
  23. François Thiré. Interoperability between proof systems using the logical framework Dedukti. PhD thesis, ENS Paris-Saclay, 2020. Google Scholar
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