en ¦ fr > Talks

A tour in (formalised) type theory

novembre 2024

Formalisation of mathematics with ITPs seminar – Cambridge, Mathematics Department

Meven Lennon-Bertrand

Slides Demo

Verified Meta-Theory at Scale for a Certified Proof Assistant

octobre 2024

Newton Institute – Big Specification Workshop

Meven Lennon-Bertrand

Slides Vidéo

Implementing Observational Equality Using Normalisation by Evaluation

juin 2024

TYPES

Matthew Sirman, Meven Lennon-Bertrand, Neel Krishnaswami

Slides Résumé

Martin-Löf à la Coq – Mechanized normalisation for a dependently typed language

juin 2024

Journée Reciprog & condition de garde

Arthur Adjedj, Meven Lennon-Bertrand, Kenji Maillard, Pierre-Marie Pédrot, Loïc Pujet

Slides

Towards a certified type theoretic kernel

avril 2024

Exposé invité – EuroProofNet, groupe de travail 6

Meven Lennon-Bertrand

Slides Vidéo

Tutoriel MetaCoq

janvier 2024

Tutorials @ POPL

Yannick Forster, Meven Lennon-Bertrand, Matthieu Sozeau, Théo Winterhalter

Slides GitHub

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

décembre 2023

PPS Seminar, Proof and Algorithms Seminar @ LIX, Deducteam Seminar

Meven Lennon-Bertrand

J'ai donné un exposé similaire au séminaire du groupe Dependable Systems à Heriot Watt University en mars 2024.

Slides

Definitional Functoriality for Dependent (Sub)Types

décembre 2023

Formath Seminar

Théo Laurent, Meven Lennon-Bertrand, Kenji Maillard

J'ai donné un exposé similaire à SPLS en mars 2024.

Slides

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

juin 2023

TYPES

Neel Krishnaswami, Meven Lennon-Bertrand

Slides Résumé

Engineering Logical Relations for MLTT in Coq

juin 2023

TYPES

Arthur Adjedj, Meven Lennon-Bertrand, Kenji Maillard, Loïc Pujet

Résumé

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