Document Open Access Logo

Expressing Ecumenical Systems in the λΠ-Calculus Modulo Theory

Author Emilie Grienenberger

PDF
Thumbnail PDF

File

LIPIcs.TYPES.2022.4.pdf
  • Filesize: 0.95 MB
  • 23 pages

Document Identifiers

Author Details

Emilie Grienenberger
  • Université Paris-Saclay, ENS Paris-Saclay, Inria, CNRS, Laboratoire Méthodes Formelles, France

Acknowledgements

The author thanks Gilles Dowek for his scientific advice and guidance, and the reviewers for their constructive and detailed returns.

Cite AsGet BibTex

Emilie Grienenberger. Expressing Ecumenical Systems in the λΠ-Calculus Modulo Theory. In 28th International Conference on Types for Proofs and Programs (TYPES 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 269, pp. 4:1-4:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.TYPES.2022.4

Abstract

Systems in which classical and intuitionistic logics coexist are called ecumenical. Such a system allows for interoperability and hybridization between classical and constructive propositions and proofs. We study Ecumenical STT, a theory expressed in the logical framework of the λΠ-calculus modulo theory. We prove soudness and conservativity of four subtheories of Ecumenical STT with respect to constructive and classical predicate logic and simple type theory. We also prove the weak normalization of well-typed terms and thus the consistency of Ecumenical STT.

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
  • Theory of computation → Proof theory
  • Theory of computation → Higher order logic
  • Theory of computation → Constructive mathematics
Keywords
  • dependent types
  • predicate logic
  • higher order logic
  • constructivism
  • interoperability
  • ecumenical logics

Metrics

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

References

  1. Claus Appel, Vincent van Oostrom, and Jakob Grue Simonsen. Higher-order (non-)modularity. In Christopher Lynch, editor, Proceedings of the 21st International Conference on Rewriting Techniques and Applications, RTA 2010, July 11-13, 2010, Edinburgh, Scottland, UK, volume 6 of LIPIcs, pages 17-32. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2010. URL: https://doi.org/10.4230/LIPIcs.RTA.2010.17.
  2. Ali Assaf. A framework for defining computational higher-order logics. (Un cadre de définition de logiques calculatoires d'ordre supérieur). PhD thesis, École Polytechnique, Palaiseau, France, 2015. URL: https://tel.archives-ouvertes.fr/tel-01235303.
  3. 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. Manuscript, 2016. Google Scholar
  4. 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.
  5. Frédéric Blanqui. Size-based termination of higher-order rewriting. Journal of Functional Programming, 28:e11, 2018. URL: https://doi.org/10.1017/S0956796818000072.
  6. Frédéric Blanqui, Gilles Dowek, Émilie Grienenberger, Gabriel Hondet, and François Thiré. Some axioms for mathematics. In Naoki Kobayashi, editor, 6th International Conference on Formal Structures for Computation and Deduction, FSCD 2021, July 17-24, 2021, Buenos Aires, Argentina (Virtual Conference), volume 195 of LIPIcs, pages 20:1-20:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPIcs.FSCD.2021.20.
  7. 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.
  8. Raphaël Cauderlier and Catherine Dubois. ML pattern-matching, recursion, and rewriting: From focalize to dedukti. In Augusto Sampaio and Farn Wang, editors, Theoretical Aspects of Computing - ICTAC 2016 - 13th International Colloquium, Taipei, Taiwan, ROC, October 24-31, 2016, Proceedings, volume 9965 of Lecture Notes in Computer Science, pages 459-468, 2016. URL: https://doi.org/10.1007/978-3-319-46750-4_26.
  9. Raphaël Cauderlier and Catherine Dubois. Focalize and dedukti to the rescue for proof interoperability. In Mauricio Ayala-Rincón and César A. Muñoz, editors, Interactive Theorem Proving - 8th International Conference, ITP 2017, Brasília, Brazil, September 26-29, 2017, Proceedings, volume 10499 of Lecture Notes in Computer Science, pages 131-147. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-66107-0_9.
  10. 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, 8th International Conference, TLCA 2007, Paris, France, June 26-28, 2007, Proceedings, volume 4583 of Lecture Notes in Computer Science, pages 102-117. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-73228-0_9.
  11. Dag Prawitz. Natural deduction, a proof-theoretical study. PhD thesis, Stockolm: Almqvist & Wicksell, 1965. Google Scholar
  12. Deducteam. Nubo, repository of interoperable formal proofs. https://deducteam.gitlabpages.inria.fr/nubo/index.html, 2020. Accessed: 2022-29-11.
  13. Alexis Dorra. Équivalence de Curry-Howard entre le lambda-Pi-calcul et la logique intuitionniste. Bachelor internship report, LIX École Polytechnique, 2011. Google Scholar
  14. Gilles Dowek. On the definition of the classical connectives and quantifiers. CoRR, 2015. URL: https://arxiv.org/abs/1601.01782.
  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. Gilles Dowek, Thérèse Hardin, and Claude Kirchner. HOL-λ σ an intentional first-order expression of higher-order logic. Mathematical Structures in Computer Science, 11(1):1-25, 2001. Google Scholar
  17. Gilles Dowek and Benjamin Werner. Proof normalization modulo. J. Symb. Log., 68(4):1289-1316, 2003. URL: https://doi.org/10.2178/jsl/1067620188.
  18. 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, August 2-5, 2022, Haifa, Israel, volume 228 of LIPIcs, pages 25:1-25:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/LIPIcs.FSCD.2022.25.
  19. Guillaume Genestier. Encoding Agda Programs Using Rewriting. In Zena M. Ariola, editor, 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020), volume 167 of Leibniz International Proceedings in Informatics (LIPIcs), pages 31:1-31:17, Dagstuhl, Germany, 2020. Schloss Dagstuhl-Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.FSCD.2020.31.
  20. Herman Geuvers. A short and flexible proof of strong normalization for the calculus of constructions. In Peter Dybjer, Bengt Nordström, and Jan M. Smith, editors, Types for Proofs and Programs, International Workshop TYPES'94, Båstad, Sweden, June 6-10, 1994, Selected Papers, volume 996 of Lecture Notes in Computer Science, pages 14-38. Springer, 1994. URL: https://doi.org/10.1007/3-540-60579-7_2.
  21. Jürgen Giesl, René Thiemann, and Peter Schneider-Kamp. The dependency pair framework: Combining techniques for automated termination proofs. In Franz Baader and Andrei Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning, 11th International Conference, LPAR 2004, Montevideo, Uruguay, March 14-18, 2005, Proceedings, volume 3452 of Lecture Notes in Computer Science, pages 301-331. Springer, 2004. URL: https://doi.org/10.1007/978-3-540-32275-7_21.
  22. Jean-Yves Girard. On the unity of logic. Ann. Pure Appl. Logic, 59(3):201-217, 1993. URL: https://doi.org/10.1016/0168-0072(93)90093-S.
  23. Jean-Yves Girard, Paul Taylor, and Yves Lafont. Proofs and types. Cambridge Tracts in Theoretical Computer Science, 7, 1989. Google Scholar
  24. 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.
  25. Robert Harper, Furio Honsell, and Gordon D. Plotkin. A framework for defining logics. In Proceedings of the Symposium on Logic in Computer Science (LICS '87), Ithaca, New York, USA, June 22-25, 1987, pages 194-204. IEEE Computer Society, 1987. Google Scholar
  26. 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, March 2-5, 2020, University of Turin, Italy, volume 188 of LIPIcs, pages 6:1-6:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. URL: https://doi.org/10.4230/LIPIcs.TYPES.2020.6.
  27. Alfred Horn. Logic with truth values in a linearly ordered heyting algebra. J. Symb. Log., 34(3):395-408, 1969. URL: https://doi.org/10.2307/2270905.
  28. Jean-Pierre Jouannaud and Jianqi Li. Termination of Dependently Typed Rewrite Rules. 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 257-272, Dagstuhl, Germany, 2015. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. URL: https://doi.org/10.4230/LIPIcs.TLCA.2015.257.
  29. Andrei Nikolaevich Kolmogorov. On the principle of the excluded middle. In Matematicheskij Sbornik, volume 32, pages 646-667, 1925. Google Scholar
  30. C.L.M. Kop. Higher Order Termination: Automatable Techniques for Proving Termination of Higher-Order Term Rewriting Systems. PhD thesis, Vrije Universiteit Amsterdam, 2012. Naam instelling promotie: VU Vrije Universiteit Naam instelling onderzoek: VU Vrije Universiteit. Google Scholar
  31. Keiichirou Kusakari and Masahiko Sakai. Enhancing dependency pair method using strong computability in simply-typed term rewriting. Appl. Algebra Eng., Commun. Comput., 18(5):407-431, October 2007. Google Scholar
  32. Chin Lee, Neil Jones, and Amir Ben-Amram. The size-change principle for program termination. ACM SIGPLAN Notices, 36, January 2001. URL: https://doi.org/10.1145/360204.360210.
  33. Chuck Liang and Dale Miller. Unifying classical and intuitionistic logics for computational control. In 28th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2013, New Orleans, LA, USA, June 25-28, 2013, pages 283-292. IEEE Computer Society, 2013. URL: https://doi.org/10.1109/LICS.2013.34.
  34. Paqui Lucio. Structured sequent calculi for combining intuitionistic and classical first-order logic. In Hélène Kirchner and Christophe Ringeissen, editors, Frontiers of Combining Systems, Third International Workshop, FroCoS 2000, Nancy, France, March 22-24, 2000, Proceedings, volume 1794 of Lecture Notes in Computer Science, pages 88-104. Springer, 2000. URL: https://doi.org/10.1007/10720084_7.
  35. 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, International Workshop TYPES'96, Aussois, France, December 15-19, 1996, Selected Papers, volume 1512 of Lecture Notes in Computer Science, pages 254-276. Springer, 1996. URL: https://doi.org/10.1007/BFb0097796.
  36. Luiz Carlos Pereira and Ricardo Oscar Rodriguez. Normalization, soundness and completeness for the propositional fragment of prawitz’ ecumenical system. In Revista Portuguesa De Filosofia 73, no. 3/4, pages 1153-1168, 2017. Google Scholar
  37. Elaine Pimentel, Luiz Carlos Pereira, and Valeria de Paiva. An ecumenical notion of entailment. Synthese, pages 1-23, 2019. URL: https://doi.org/10.1007/s11229-019-02226-5.
  38. Dag Prawitz. Classical versus intuitionnistic logic. In Edward Hermann Haeusler, Wagner de Campos Sanz, Bruno Lopes, and College Publications, editors, Why is this a proof ? Festschrift for Luiz Carlos Pereira, pages 15-32, 2015. Google Scholar
  39. Raphaël Cauderlier. Sigmaid. https://gitlab.math.univ-paris-diderot.fr/cauderlier/sigmaid, 2014. Accessed: 2022-29-11.
  40. Ronan Saillard. Typechecking in the lambda-Pi-Calculus Modulo : Theory and Practice. (Vérification de typage pour le lambda-Pi-Calcul Modulo : théorie et pratique). PhD thesis, Mines ParisTech, France, 2015. URL: https://tel.archives-ouvertes.fr/tel-01299180.
  41. William W. Tait. Intensional interpretations of functionals of finite type I. J. Symb. Log., 32(2):198-212, 1967. URL: https://doi.org/10.2307/2271658.
  42. Terese. Term rewriting systems, volume 55 of Cambridge tracts in theoretical computer science. Cambridge University Press, 2003. Google Scholar
  43. François Thiré. Sharing a Library between Proof Assistants: Reaching out to the HOL Family. Electronic Proceedings in Theoretical Computer Science, 274:57-71, July 2018. URL: https://doi.org/10.4204/EPTCS.274.5.
  44. François Thiré. Interoperability between proof systems using the logical framework Dedukti. (Interopérabilité entre systèmes de preuve en utilisant le cadre logique Dedukti). PhD thesis, École normale supérieure Paris-Saclay, Cachan, France, 2020. URL: https://tel.archives-ouvertes.fr/tel-03224039.
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