### Myself

I am currently a postdoc at the MPI for Security and Privacy in Bochum, working with Cătălin Hrițcu. Previously, I was 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 from the MPRI (Parisian Master in Computer Science).

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

You can contact me at `firstname.lastname@csp.mpg.de`

.

##### Experience

##### Internships

#### 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

### PhD thesis

#### Formalisation and Meta-Theory of Type Theory

In this thesis, I talk about the meta-theory of type theory and about how to formalise it in a proof assistant.

I first focus on a conservative translation between extensional type theory and either intensional or weak type theory, entirely written in Coq. The first translation consists in a removal of the reflection of equality rule, whereas the second translation produces something stronger: weak type theory is a type theory with no notion of conversion. The conservativity result implies that conversion doesn't increase the logical power of type theories.

Then, I show my work for the MetaCoq project of formalising and specifying Coq within Coq. In particular I worked on writing a type-checker for Coq, in Coq. This type checker is proven sound with respect to the specification and can be extracted to OCaml code and run independently of Coq's kernel type-checker. For this to work we have to rely on the meta-theory of Coq which we develop, in part, in the MetaCoq project. However, because of Gödel's incompleteness theorems, we cannot prove consistency of Coq within Coq, and this means that some properties—mainly strong normalisation—have to be assumed, i.e. taken as axioms.

Defended on 18 Sept 2020

### Research articles

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

Jesper Cockx, Nicolas Tabareau, Théo Winterhalter (2021)

POPL

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

Matthieu Sozeau, Simon Boulier, Yannick Forster, Nicolas Tabareau, Théo Winterhalter (2020)

POPL

#### The MetaCoq Project

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

JAR

#### Eliminating Reflection from Type Theory

Théo Winterhalter, Matthieu Sozeau, Nicolas Tabareau (2019)

CPP

#### Normalization by evaluation for sized dependent types

Andreas Abel, Andrea Vezzosi, Théo Winterhalter (2017)

ICFP

#### Randomized Mixed-Radix Scalar Multiplication

Eleonora Guerrini, Laurent Imbert, Théo Winterhalter (2017)

IEEE Transactions on Computers

### Talks

#### Cancelled Modular Confluence for Rewrite Rules in MetaCoq

Jesper Cockx, Nicolas Tabareau and Théo Winterhalter

TYPES 2020

#### Weak Type Theory is Rather Strong

Théo Winterhalter and Simon Boulier

TYPES 2019

#### How to Tame your Rewrite Rules

Jesper Cockx, Nicolas Tabareau and Théo Winterhalter

TYPES 2019

#### Using reflection to eliminate reflection

Théo Winterhalter, Matthieu Sozeau and Nicolas Tabareau

EUTypes Aarhus

#### Using reflection to eliminate reflection

Théo Winterhalter, Matthieu Sozeau and Nicolas Tabareau

TYPES 2018

#### A modular formalization of type theory in Coq

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

TYPES 2017

#### Normalization by Evaluation for Sized Dependent Types

Andreas Abel, Andrea Vezzosi and Théo Winterhalter

TYPES 2017

#### The rules of type theory

Théo Winterhalter, Andrej Bauer, Philipp 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 and Andreas Abel

TYPES 2016

### Projects

#### ett-to-itt

Formalisation of a translation from ETT to ITT

#### MetaCoq

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

#### formal-type-theory

Modular formalisation of type theory (rather old)

#### ogaml

Ocaml graphics and multimedia library

#### docaml

Automatic documentation generation for ocaml