For my masters thesis I worked as an intern under the supervision of Nicolas Tabareau. We collaborated with Éric Tanter on applying the gradual typing approach to the Calculus of Inductive Constructions. Although the internship led to a thesis and defence, those are outdated – see the corresponding publication instead.
Coalgebraic determinization of alternating automata
During my master’s first year, I was an intern with Jurriaan Rot. We worked on alternating automata in a coalgebraic approach.
Compilation of Dependent Pattern-Matching without Axiom K
At the end of my bachelors, I was an intern for 2 months with Hugo Herbelin. We worked on an algorithm to compile complex, dependent pattern-matching without using the axiom K, following ideas around small inversion.