en ¦ fr > Internships

Gradualizing the Calculus of Inductive Constructions

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.

Pdf Slides

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.

Pdf Slides

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.

Pdf Slides

Under Creative Commons CC0 License, source on github. Built using Pelican. Theme adapted from pelican-svbhack by Giulio Fidente.