In the spring semester of 2019 I was an intern under the supervision of Nicolas Tabareau. We worked with Éric Tanter on applying the gradual typing approach to the Calculus of Inductive Constructions. Although the internship led to a thesis and defense, those are outdated – see the corresponding draft publication instead.

During the spring semester of 2017, I was an intern with Jurriaan Rot. We worked on alternating automata in a coalgebraic approach. The report is published on arXiv.

In 2016, 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. It did not make it to any kind of publication for now.