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.
I will give a talk about dependent ghosts at the CHoCoLa meeting in Lyon, on 21 November.
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

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. Rewrite rules in Coq and SProp in MetaCoq.

Interns

Ewen Broudin–Caradec. Ghost dependent types. Masters internship (4.5 months, 2024) Formalisation
Yann Leray. Rewrite rules in Coq and MetaCoq. Predoctoral internship (8 months, 2022/2023) Now: PhD student with Nicolas Tabareau, Matthieu Sozeau, and me. Coq with rewrite rules

Internships

Feel free to contact me if you want to do an internship with me. We can discuss subjects and I have several potential projects in mind. Below is one such proposal, primarily intended for an M2 internship, but I have other topic that involve e.g. partially defined, potentially non-terminating functions and MetaCoq, or definitional equality in Dedukti.

Local extensions of type theory with new definitional equalities

Coq has recently been extended with rewrite rules so that a user can declare new computations for freshly introduced symbols. For instance one can declare an addition on natural numbers such that n + 0 and 0 + n both reduce to n. For now such rewrite rules are global, meaning one has to keep them in scope forever after they are introduced. Local rewrite rules would allow one to only extend definitional equality in a specific definition (similar to how one can do a λ-abstraction to locally assume some proposition), and then instantiate them later.

Publications

Peer-reviewed publications and drafts

The Rewster: Type Preserving Rewrite Rules for the Coq Proof Assistant

Yann Leray, Gaëtan Gilbert, Nicolas Tabareau and Théo Winterhalter

ITP (2024)

PDF Bibtex

Dependent Ghosts Have a Reflection for Free

Théo Winterhalter

ICFP (2024)

PDF Bibtex Formalisation

Draft Correct and Complete Type Checking and Certified Erasure for Coq, in Coq

Matthieu Sozeau, Yannick Forster, Meven Lennon-Bertrand, Jakob Botsch Nielsen, Nicolas Tabareau, and Théo Winterhalter

2024

PDF Bibtex Formalisation

Impredicativity, Cumulativity and Product Covariance in the Logical Framework Dedukti

Thiago Felicissimo, and Théo Winterhalter

2024

PDF Bibtex

From Rewrite Rules to Axioms in the λΠ-Calculus Modulo Theory

Valentin Blot, Gilles Dowek, Thomas Traversié, and Théo Winterhalter

2024

PDF Bibtex

Securing Verified IO Programs Against Unverified Code in F*

Cezar-Constantin Andrici, Stefan Ciobaca, Cătălin Hrițcu, Guido Martínez, Exequiel Rivas, Éric Tanter, and Théo Winterhalter

2024

PDF Bibtex F* development

The Last Yard: Foundational End-to-End Verification of High-Speed Cryptography

Philipp G. Haselwarter, Benjamin Salling Hvass, Lasse Letager Hansen, Théo Winterhalter, Cătălin Hrițcu, and Bas Spitters

2024

PDF Bibtex Formalisation

SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq

Philipp G. Haselwarter, Exequiel Rivas, Antoine Van Muylder, Théo Winterhalter, Carmine Abate, Nikolaj Sidorenco, Cătălin Hrițcu, Kenji Maillard, and Bas Spitters

2023

PDF Bibtex Formalisation