Combining computational theories
Monday 3 February 2025 at 14h30
ENS Paris-Saclay, Room 1Z14
Abstract. Proof checkers and proof assistants are used to formalize mathematical theorems and verify software, notably critical systems such as medical, industrial and transport systems. The diversity of proof systems raises the question of their interoperability: how can proofs be rechecked and reused across systems? Logical frameworks such as the λΠ-calculus modulo theory provide a common formalism in which various logical systems and mathematical theories can be expressed. The proof transformation tools within the λΠ-calculus modulo theory allow proofs to be translated from one logical system another. In a similar way to logical frameworks, theories combining several theories provide a common language between theories. The main focus of this manuscript is the study of the definition and properties of these theories, specifically in the context of computational theories, that is whose definition relies on rewriting. More specifically, combinations of computational theories will be studied in two contexts: ecumenical logics, i.e. logics that combine intuitionistic and classical logics, and theories of pure type systems modulo rewriting, which are used in the λΠ-calculus modulo theory to express logical systems of various proof assistants. First, we look at the special case of ecumenical logics, i.e. logics that combine intuitionistic and classical logics. A new ecumenical logic called NE is defined and studied. Its main properties are that its definition, though guided by, does not rely on double negations, and that it allows the definition of computational ecumenical theories, such as an ecumenical simple type theory.
In a second time, the computational theories of pure type systems, an example of which is the logical framework of the λΠ-calculus modulo theory, are studied. In particular, we give tools to establish the well typedness of computational theories in a modular way, whether for extension or restriction (called fragmentation) of theories. Finally, we prove that for a given proof in a theory combining multiple fragments, it is possible to establish to which fragment this proof belongs from the constants it contains, without explicit indications of the rewriting rules used. This result is crucial in justifying the use of such theories for the interoperability of proof systems.
Finally, based on the definition of NE and the previous modularity results, we focus on a computational theory of λΠ-calculus called theory U, combining first- and higher-order logics, minimal, intuitionistic, classical and ecumenical logics, prenex polymorphism and predicate subtyping, and the calculus of constructions. Properties of soundness, conservativity, consistency, normalization, and decidability of type-checking are established for the first- and higher-order logical fragments of theory U.
Thesis supervisors: Gilles Dowek, Dale Miller
Jury:
- Valeria de Paiva, Rapportrice & Examinatrice
- Cezary Kaliszyk, Rapporteur & Examinateur
- Elaine Pimentel, Examinatrice
- Jean-Baptiste Joinet, Examinateur
- Assia Mahboubi, Examinatrice