en ¦ fr > Exposés

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é

Equivalence Between Typed and Untyped Conversion

juin 2022

TYPES

Meven Lennon-Bertrand

Slides Vidéo Résumé

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

janvier 2022

WITS

Matthieu Sozeau, Meven Lennon-Bertrand, Yannick Forster

Vidéo

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

janvier 2022

WITS

Meven Lennon-Bertrand

Slides Vidéo Résumé

Gradualizing the Calculus of Inductive Constructions

janvier 2022

TOPLAS journal-first presentation @ POPL

Slides Vidéo

Un calcul des constructions graduel

février 2021

Journées LHC

Meven Lennon-Bertrand

Slides Web Page

Gradualizing the Calculus of Inductive Constructions

janvier 2021

CPP Lightning Talk

Meven Lennon-Bertrand

Slides Vidéo

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