en ¦ fr > Talks

À bas l’η — Coq’s troublesome η-conversion

Where I report on the difficulties presented by the treatment of η-conversion in the setting of the MetaCoq project, try and give insight on why the situation is surprisingly thorny in that specific setting, and consider what we could do to get out of this.

Slides Page Abstract

Gradualizing the Calculus of Inductive Constructions

Presentation of our TOPLAS article in the journal-first track of POPL.

Slides Page

Un calcul des constructions graduel

Slides Page

Gradualizing the Calculus of Inductive Constructions

Short presentation of work in progress on our TOPLAS article.

Slides Video

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