I am a researcher in Deducteam at INRIA Saclay and at the LMF located at ENS Paris-Saclay.
Previously I was a postdoctoral researcher at Max Planck Institute for Security and Privacy (MPI-SP) in Bochum (Germany), working with Cătălin Hrițcu. Before that I completed a PhD within Gallinette in Nantes, with Nicolas Tabareau and Matthieu Sozeau.
My main interest lies in type theory and proof assistants. As such, most of my results are formalised in a proof assistant, generally Coq. I strive to make proof assistants better and safer.
News
- I will be part of the PC of ICFP 2025.
- I will be part of the PC of TYPES 2025.
- Our paper Correct and Complete Type Checking and Certified Erasure for Coq, in Coq with Matthieu Sozeau, Yannick Forster, Meven Lennon-Bertrand, Jakob Botsch Nielsen and Nicolas Tabareau was accepted for the Journal of the ACM.
- Because having a personal page is essential for academia, but because it’s annoying to set up for some, Yannick Forster and I created a template that you can use and customise very easily.
Older news
- I gave a talk about dependent ghosts at the CHoCoLa meeting in Lyon, on 21 November.
- Clément Pit-Claudel and I organised the Coq Workshop 2024.
Teaching
I teach the Proof assistants course of the MPRI together with Yannick Forster.
PhD students
Yann Leray
Co-supervised with Nicolas Tabareau and Matthieu Sozeau. Located in Nantes.
Rewrite rules in Coq and SProp in MetaCoq.
Past Interns
Ewen Broudin–Caradec
Ghost dependent types.
Masters internship (4.5 months, 2024).
Yann Leray
Rewrite rules in Coq and MetaCoq.
Predoctoral internship (8 months, 2022/2023)
Now: PhD student with Nicolas Tabareau, Matthieu Sozeau, and me.
Publications
Peer-reviewed publications and drafts
Correct and Complete Type Checking and Certified Erasure for Coq, in Coq
JACM (2024)
The Rewster: Type Preserving Rewrite Rules for the Coq Proof Assistant
ITP (2024)
Dependent Ghosts Have a Reflection for Free
ICFP (2024)
Impredicativity, Cumulativity and Product Covariance in the Logical Framework Dedukti
FSCD (2024)
From Rewrite Rules to Axioms in the λΠ-Calculus Modulo Theory
FoSSaCS (2024)
Securing Verified IO Programs Against Unverified Code in F*
POPL (2024)
The Last Yard: Foundational End-to-End Verification of High-Speed Cryptography
CPP (2024)
SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq
TOPLAS — Extended version of the CSF paper (2023)
Distinguished SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq
CSF (2021)
The Taming of the Rew: A Type Theory with Computational Assumptions
POPL (2021)
Coq Coq Correct! Verification of Type Checking and Erasure for Coq, in Coq
POPL (2020)
The MetaCoq Project
JAR (2020)
Eliminating Reflection from Type Theory
CPP (2019)
Normalization by evaluation for sized dependent types
ICFP (2017)
Randomized Mixed-Radix Scalar Multiplication
IEEE Transactions on Computers (2017)
PhD thesis
Formalisation and meta-theory of type theory
Gallinette Inria team, LS2N, University of Nantes (2020)
International seminars (mostly peer-reviewed)
Invited talk Dependent Ghosts Have a Reflection for Free
Chocola, Lyon (2024)
Towards a logical framework modulo rewriting and equational theories
TYPES (2024)
Dependent Ghosts Have a Reflection for Free
EuroProofNet WG6 (2024)
The Rewster: The Coq Proof Assistant with Rewrite Rules
TYPES (2023)
Composable partial functions in Coq, totally for free
TYPES (2023)
Invited talk A conservative and constructive translation from extensional type theory to weak type theory
Strength of Weak Type Theory, Amsterdam (2023)
Securely Compiling F* Programs With IO and Then Linking Them Against Weakly-Typed Interfaces
PriSC (2023)
Verifying non-terminating programs with IO in F*
HOPE (2022)
Partial Dijkstra Monads for All
TYPES (2022)
Invited talk MetaCoq: Sound and complete type checking for Coq, in Coq
SSTT Stockholm (EuroProofNet WG6) (2022)
SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq
Coq workshop (2021)
Shape-irrelevant reflection: terminating extensional type theory
TYPES (2021)
SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq
TYPES (2021)
Modular Confluence for Rewrite Rules in MetaCoq
TYPES (cancelled) (2020)
Weak Type Theory is Rather Strong
TYPES (2019)
How to Tame your Rewrite Rules
TYPES (2019)
Using reflection to eliminate reflection
EUTypes Aarhus (2018)
Using reflection to eliminate reflection
TYPES (2018)
A modular formalization of type theory in Coq
TYPES (2017)
Normalization by Evaluation for Sized Dependent Types
TYPES (2017)
The rules of type theory
Workshop on Syntax and Semantics of Type Theory, Ljubljana (2017)
An Extension of Martin-Löf Type Theory with Sized Types
TYPES (2016)