News

I was a PhD student of Nicolas Tabareau and Matthieu Sozeau within the Inria team Gallinette at LS2N in Nantes (France). In this thesis, I talk about the meta-theory of type theory and about how to formalise it in a proof assistant. I have worked on several topics during my PhD. I first worked on the relation between extensional type theory and intensional type theory. This work is then extended to weak type theory. Another big part of my thesis is about verifying a type-checker for Coq, in Coq itself. Finally, although it is not part of my manuscript, I have also worked on safely extending the theory of Coq or Agda with user-defined rewrite rules.

PDF LaTeX Bibtex Defence video

Extensional type theory (ETT) is distinguished from regular intensional type theory (ITT) in that it features the reflection of equality rule. This rule states that any provable equality can be considered as conversion. This rule is really practical when formalising mathematics or programming with dependent types. Its presence however makes type-checking undecidable. Martin Hofmann showed categorically that ETT is conservative over ITT (meaning that any statement in ITT that is a theorem in ETT is also a theorem in ITT). Ten years later, Nicolas Oury furthered this result by proposing a translation from ETT to ITT. We complete this work by providing an effective translation (in the sense of a Coq program) with minimal axiom use.

Eliminating Reflection from Type Theory

with Matthieu Sozeau and Nicolas Tabareau

CPP (2019)

PDF Bibtex Slides Formalisation

Simon Boulier and I noticed that the translation above did not make any use of conversion in the target, ITT. As such we proposed an extension of the conservativity result to conservativity of ETT over weak type theory (WTT). WTT does not feature any notion of conversion whatsoever. Instead all computation rules are treated propositionally, as special equality proofs. In particular, this shows that ITT is also conservative over WTT.

Formalisation

Using the MetaCoq representation and specification of Coq itself, we define a type-checker for Coq and prove it correct and terminating, assuming strong normalisation of the theory. This shifts the trusted base from the complex implementation to the relatively simpler theory.

Coq Coq Correct! Verification of Type Checking and Erasure for Coq, in Coq

with Matthieu Sozeau, Simon Boulier, Yannick Forster and Nicolas Tabareau

POPL (2020)

PDF Bibtex Video Slides Formalisation

Computation is very practical in dependent type theories to automatically simplify expressions during type-checking. Type theories do not always feature everything the user wants and as such it is common for them to postulate extra principles in the form of axioms. Those axioms however do not feature any computational behaviour. To avoid having to rely on the reflection rule, a middle ground can be to also postulate computational behaviours for those axioms in the form of rewrite rules. We propose an extension of MetaCoq with rewrite rules, as well as a criterion that ensures we preserve confluence and subject reduction.

The Taming of the Rew: A Type Theory with Computational Assumptions

with Jesper Cockx and Nicolas Tabareau

POPL (2021)

PDF Bibtex Formalisation Video

Experience and education

Community service

I was a member of the following program committees: CPP 2024, POPL 2023, HoTT/UF workshop 2022, HoTT/UF workshop (2023). I have been a member of the Artifact Evaluation Committee of ICFP18.

Education

I was a computer science student at ENS Cachan and graduated from the MPRI (Parisian Master in Computer Science). During that time I did five internships: 2 months with Laurent Imbert and Eleonora Guerrini, 5 with Andreas Abel, 5 with Nicolas Tabareau, 6 with Andrej Bauer, and 4 with Matthieu Sozeau.