My picture

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

Older news

Teaching

MPRI PRFA

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).

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

Publications

Peer-reviewed publications and drafts

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

JACM (2024)

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

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

ITP (2024)

Dependent Ghosts Have a Reflection for Free

Théo Winterhalter

ICFP (2024)

Impredicativity, Cumulativity and Product Covariance in the Logical Framework Dedukti

Thiago Felicissimo, and Théo Winterhalter

FSCD (2024)

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

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

FoSSaCS (2024)

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

POPL (2024)

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

CPP (2024)

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

TOPLAS — Extended version of the CSF paper (2023)

Distinguished SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq

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

CSF (2021)

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

Jesper Cockx, Nicolas Tabareau, and Théo Winterhalter

POPL (2021)

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

Matthieu Sozeau, Simon Boulier, Yannick Forster, Nicolas Tabareau, and Théo Winterhalter

POPL (2020)

The MetaCoq Project

Matthieu Sozeau, Abhishek Anand, Simon Boulier, Cyril Cohen, Yannick Forster, Fabian Kunze, Gregory Malecha, Nicolas Tabareau, and Théo Winterhalter

JAR (2020)

Eliminating Reflection from Type Theory

Théo Winterhalter, Matthieu Sozeau, and Nicolas Tabareau

CPP (2019)

Normalization by evaluation for sized dependent types

Andreas Abel, Andrea Vezzosi, and Théo Winterhalter

ICFP (2017)

Randomized Mixed-Radix Scalar Multiplication

Eleonora Guerrini, Laurent Imbert, and Théo Winterhalter

IEEE Transactions on Computers (2017)

PhD thesis

Formalisation and meta-theory of type theory

Supervised by Nicolas Tabareau and Matthieu Sozeau

Gallinette Inria team, LS2N, University of Nantes (2020)

International seminars (mostly peer-reviewed)

Invited talk Dependent Ghosts Have a Reflection for Free

Théo Winterhalter

Chocola, Lyon (2024)

Towards a logical framework modulo rewriting and equational theories

Bruno Barras , Thiago Felicissimo, Théo Winterhalter

TYPES (2024)

Dependent Ghosts Have a Reflection for Free

Théo Winterhalter

EuroProofNet WG6 (2024)

The Rewster: The Coq Proof Assistant with Rewrite Rules

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

TYPES (2023)

Composable partial functions in Coq, totally for free

Théo Winterhalter

TYPES (2023)

Invited talk A conservative and constructive translation from extensional type theory to weak type theory

Théo Winterhalter

Strength of Weak Type Theory, Amsterdam (2023)

Securely Compiling F* Programs With IO and Then Linking Them Against Weakly-Typed Interfaces

Cezar-Constantin Andrici , Cătălin Hrițcu, Théo Winterhalter

PriSC (2023)

Verifying non-terminating programs with IO in F*

Cezar-Constantin Andrici , Théo Winterhalter, Cătălin Hrițcu, Exequiel Rivas

HOPE (2022)

Partial Dijkstra Monads for All

Théo Winterhalter Cezar-Constantin Andrici, Cătălin Hrițcu, Kenji Maillard, Guido Martínez, Exequiel Rivas

TYPES (2022)

Invited talk MetaCoq: Sound and complete type checking for Coq, in Coq

Théo Winterhalter and the MetaCoq team

SSTT Stockholm (EuroProofNet WG6) (2022)

SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq

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

Coq workshop (2021)

Shape-irrelevant reflection: terminating extensional type theory

Théo Winterhalter

TYPES (2021)

SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq

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

TYPES (2021)

Modular Confluence for Rewrite Rules in MetaCoq

Jesper Cockx, Nicolas Tabareau, Théo Winterhalter

TYPES (cancelled) (2020)

Weak Type Theory is Rather Strong

Théo Winterhalter , Simon Boulier

TYPES (2019)

How to Tame your Rewrite Rules

Jesper Cockx , Nicolas Tabareau, Théo Winterhalter

TYPES (2019)

Using reflection to eliminate reflection

Théo Winterhalter , Matthieu Sozeau, Nicolas Tabareau

EUTypes Aarhus (2018)

Using reflection to eliminate reflection

Théo Winterhalter , Matthieu Sozeau, Nicolas Tabareau

TYPES (2018)

A modular formalization of type theory in Coq

Andrej Bauer , Philipp G. Haselwarter, Théo Winterhalter

TYPES (2017)

Normalization by Evaluation for Sized Dependent Types

Andreas Abel , Andrea Vezzosi, Théo Winterhalter

TYPES (2017)

The rules of type theory

Théo Winterhalter , Andrej Bauer, Philipp G. Haselwarter,

Workshop on Syntax and Semantics of Type Theory, Ljubljana (2017)

An Extension of Martin-Löf Type Theory with Sized Types

Théo Winterhalter , Andreas Abel

TYPES (2016)