en ¦ fr > Talks

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

Résumé

Ingeneering Logical Relations for MLTT in Coq

Résumé

Sous Licence Creative Commons CC0, source sur github. Développé avec Pelican. Thème adapté de pelican-svbhack par Giulio Fidente.