Combining computational theories
Monday 3rd February, at 14h30
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 lambdaPi-calculus modulo theory provide a common formalism in which various logical systems and mathematical theories can be expressed. The proof transformation tools within the lambdaPi-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 thesis 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 lambdaPi-calculus modulo theory to express logical systems of various proof assistants.
Jury:
- Valeria de Paiva, Topos Institute - Rapportrice
- Cezary Kaliszyk, The University of Melbourne - Rapporteur
- Elaine Pimentel, UCL Computer Science - Examinatrice
- Assia Mahboubi, Inria - Examinatrice
- Jean-Baptiste Joinet, Université Jean Moulin - Examinateur
- Gilles Dowek, Inria - Directeur
- Dale Miller, Inria - Co-encadrant