en ¦ fr > Talks

What does it take to certify a conversion checker?

July 2025

FSCD 2025

Meven Lennon-Bertrand

Slides

AdapTT: A Type Theory with Functorial Types

June 2025

TYPES

Arthur Adjedj, Thibaut Benjamin, Meven Lennon-Bertrand, Kenji Maillard

Slides Video

A tour in (formalised) type theory

November 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

October 2024

Newton Institute – Big Specification Workshop

Meven Lennon-Bertrand

Slides Video

Implementing Observational Equality Using Normalisation by Evaluation

June 2024

TYPES

Matthew Sirman, Meven Lennon-Bertrand, Neel Krishnaswami

Slides Abstract

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

June 2024

Reciprog & Guard Condition Day

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

Slides

Towards a certified type theoretic kernel

April 2024

Invited Talk – EuroProofNet Working Group 6

Meven Lennon-Bertrand

Slides Video

MetaCoq tutorial

January 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

December 2023

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

Meven Lennon-Bertrand

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

Slides

Definitional Functoriality for Dependent (Sub)Types

December 2023

Formath Seminar

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

I gave a similar talk at SPLS in March 2024.

Slides

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

June 2023

TYPES

Neel Krishnaswami, Meven Lennon-Bertrand

Slides Abstract

Engineering Logical Relations for MLTT in Coq

June 2023

TYPES

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

Abstract

Equivalence Between Typed and Untyped Conversion

June 2022

TYPES

Meven Lennon-Bertrand

Slides Video Abstract

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

January 2022

WITS

Matthieu Sozeau, Meven Lennon-Bertrand, Yannick Forster

Video

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

January 2022

WITS

Meven Lennon-Bertrand

Slides Video Abstract

Gradualizing the Calculus of Inductive Constructions

January 2022

TOPLAS journal-first presentation @ POPL

Meven Lennon-Bertrand, Kenji Maillard, Nicolas Tabareau, Éric Tanter

Slides Video

Un calcul des constructions graduel

February 2021

Journées LHC

Meven Lennon-Bertrand

Slides Web Page

Gradualizing the Calculus of Inductive Constructions

January 2021

CPP Lightning Talk

Meven Lennon-Bertrand

Slides Video

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