en ¦ fr > Talks

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 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.