Translations of Proofs between Higher-Order Logics and between Theories with Rewriting
Thursday, 24 September 2026 at 2pm
Amphi 1, Eiffel building, CentraleSupélec, Gif-sur-Yvette
Abstract: Formal proofs and proof assistants are rigorous tools for expressing theorems and verifying their validity. Formal proofs can be based on a wide variety of logics, implemented in various proof assistants, and use numerous data structures or representations. The goal of this thesis is to design translations of formal proofs between such formalisms.
The first part of this thesis focuses on the translations between higher-order classical, intuitionistic and minimal logics. We extend double-negation translations from first-order logic to higher-order logic, showing that some results, that are valid in first-order logic, do not necessarily hold. Moreover, we define a translation, parameterized by monad operators, that can be instantiated to translate higher-order classical logic into intuitionistic logic, or higher-order intuitionistic logic into minimal logic. This translation also allows us to constructivize proofs of higher-order coherent formulas. Finally, we define a higher-order infinitary logic, and study it at both the syntactic and semantic level. We extend Barr's theorem to this logic, allowing us to constructivize proofs of higher-order geometric formulas. Logical frameworks are meta-languages designed for expressing logics and deductive systems.
The second part of this thesis focuses on the translations between theories of the lambdaPi-calculus modulo rewriting, a specific logical framework, whose implementation Dedukti is used as a middleware between proof systems. As a case study, we adapt a double-negation translation to this logical framework, and develop a tool that implements it in Dedukti. Furthermore, we extend theory morphisms and logical relations to the lambdaPi-calculus modulo rewriting. These translation templates can be instantiated to mechanically generate translations between theories. Provided that the parameters supplied by the user are correct, the correctness of the generated translations is guaranteed. We show how rewriting can be leveraged when applying these templates, using the example of a translation from a typed logic to an untyped logic. We develop a tool that implements such translation templates in Dedukti.
We show that existing (1+1)D and (3+1)D QED QCAs suffer from fermion doubling, and introduce a flavor-staggering-only method that resolves this while preserving chiral symmetry and circumventing the Nielsen–Ninomiya no-go theorem. We then derive a closed-form discrete-time propagator for the (1+1)D Dirac QCA and compute the two-point correlation function for the flavor-fixed model.
Applying the flavor-staggering method to the lattice Schwinger model, we construct a gauge-invariant axial charge, compute the chiral anomaly dynamically a lattice, and provide a geometric realization via a topological-insulator embedding.
Supervisors: Marc Aiguier, Gilles Dowek, and Olivier Hermant
Jury
- Assia Mahboubi, Directrice de recherche, Inria et Nantes Université, Rapportrice & Examinatrice
- Frank Pfenning, Professeur, Carnegie Mellon University, Rapporteur & Examinateur
- Delia Kesner, Professeure des universités, Université Paris Cité, Examinatrice
- Sara Negri, Professeure, University of Genoa, Examinatrice
- Elaine Pimentel, Professeure, University College London, Examinatrice
- Xavier Urbain, Professeur des universités, Lyon 1 Université, Examinateur