Théo Winterhalter

PhD Student within the team Gallinette


I am currently a PhD student of Nicolas Tabareau and Matthieu Sozeau within the Inria team Gallinette at LS2N in Nantes. Before, I was a computer science student at ENS Cachan and graduated for the MPRI (Parisian Master in Computer Science).

My research interests mainly lie in Type Theory and Proof Theory.

You can contact me at


Member of the Artifact Evaluation Committee of ICFP18


On Extensional Type Theory

with Matthieu Sozeau, at IRIF (Paris 7)

April 2017 — July 2017

On ETT and formalisation of Type Theory

with Andrej Bauer at University of Ljubljana

October 2016 — March 2017

On Resizing Rules and ETT

with Nicolas Tabareau at IMT Atlantique

March 2016 — July 2016

On Sized Types

with Andreas Abel at Chalmers / Gothenburg University

March 2015 — July 2015

On covering systems of congruence to defeat side-channel attacks

with Laurent Imbert and Eleonora Guerrini at LIRMM

June 2014 — July 2014

Research articles

The MetaCoq Project

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



The rules of type theory

Théo Winterhalter, Andrej Bauer, Philipp Haselwarter

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



Metaprogramming in Coq (my contributions are mainly focused on soundness of a type checker for Coq itself)


Ocaml graphics and multimedia library


Automatic documentation generation for ocaml