eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2023-07-28
4:1
4:23
10.4230/LIPIcs.TYPES.2022.4
article
Expressing Ecumenical Systems in the λΠ-Calculus Modulo Theory
Grienenberger, Emilie
1
Université Paris-Saclay, ENS Paris-Saclay, Inria, CNRS, Laboratoire Méthodes Formelles, France
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol269-types2022/LIPIcs.TYPES.2022.4/LIPIcs.TYPES.2022.4.pdf
dependent types
predicate logic
higher order logic
constructivism
interoperability
ecumenical logics