en ¦ fr > Talks

MetaCoq tutorial

Slides GitHub

Towards a certified proof assistant kernel – What it takes and what we have

I gave a similar talk at the Dependable Systems group's seminar at Heriot Watt University in March 2024.

Slides

Definitional Functoriality for Dependent (Sub)Types

I gave a similar talk at SPLS in March 2024.

Slides

Decidable Type-Checking for Bidirectional Martin-Löf Type Theory

Slides Abstract

Engineering Logical Relations for MLTT in Coq

Abstract

Equivalence Between Typed and Untyped Conversion

Slides Video Abstract

The Curious Case of Case – Correct & Efficient Representation of Case Analysis in Coq and MetaCoq

Video

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

Slides Video Abstract

Gradualizing the Calculus of Inductive Constructions

Slides Video

Un calcul des constructions graduel

Slides Web Page

Gradualizing the Calculus of Inductive Constructions

Slides Video

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