Loïc Pujet

I am an associate professor (maître de conférences) in the ICube laboratory of the University of Strasbourg. My research interests lie mainly in type theory, proof assistants, homotopy theory and constructive mathematics. Here is a picture of me.

You can contact me at .l?o+i8ch@^pdurrj*egt2.zf6r! .

News
19/05/2026 – Our papers Definitional proof irrelevance made accessible and Cellular methods in homotopy type theory were accepted to LICS'2026. I updated the preprints and added links to the accompanying formalisations.
08/05/2026 – I uploaded the slides for my talk at TYPES 2026.
10/04/2026 – I am co-chair of The Rocqshop 2026, which will take place in Lisbon, Portugal as part of FLoC. Submissions are open until May 27 (extended), and work in progress is very welcome!
03/02/2026 – I uploaded a preprint about accessibility and definitional proof-irrelevance, written in collaboration with Thiago Felicissimo, Yann Leray, Nicolas Tabareau, Éric Tanter and Théo Winterhalter.
26/01/2026 – I am co-chair of HoTT/UF 2026, which will take place in Aarhus, Denmark. Please consider submitting a 2-page abstract!
01/09/2025 – I started working as a maître de conférences in the ICube laboratory of the University of Strasbourg.

Research

Publications and Preprints

Definitional Proof Irrelevance Made Accessible PDF HAL Formalisation

Thiago Felicissimo, Yann Leray, Loïc Pujet, Nicolas Tabareau, Éric Tanter, Théo Winterhalter

LICS 2026

Cellular Methods in Homotopy Type Theory PDF Formalisation

Axel Ljungström, Loïc Pujet

LICS 2026

Type Theory in Type Teory Using a Strictified Syntax PDF Formalisation

Ambrus Kaposi, Loïc Pujet

ICFP 2025

Martin-Löf à la Coq PDF HAL Formalisation

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

CPP 2024 (distinguished paper)

Impredicative Observational Equality PDF HAL Formalisation

Loïc Pujet, Nicolas Tabareau

POPL 2023

Observational Equality: Now For Good PDF HAL Formalisation

Loïc Pujet, Nicolas Tabareau

POPL 2022 (distinguished paper)

Cubical Synthetic Homotopy Theory PDF HAL Formalisation

Anders Mörtberg, Loïc Pujet

CPP 2020

PhD thesis

Computing with Extensionality Principles in Type Theory PDF Github slides

PhD thesis, Nantes University, 2022

Talks

Definitional Proof Irrelevance Made Accessible slides abstract

On joint work with Thiago Felicissimo, Yann Leray, Nicolas Tabareau, Éric Tanter, Théo Winterhalter

TYPES 2026

Strictifying Categories with Families slides

On joint work with Ambrus Kaposi

SCALP 2024

A Constructive Cellular Approximation Theorem slides abstract

On joint work with Axel Ljungström

TYPES 2024

Choice Principles in Observational Type Theory slides

Stockholm-Gothenburg joint seminar (2023)

Engineering Logical Relations for MLTT in Coq abstract

Talk by Kenji Maillard on j.w.w Arthur Adjedj, Meven Lennon-Bertrand and Kenji Maillard

TYPES 2023

Mechanising Reducibility Proofs in Coq slides

Invited talk

Europroofnet Working Group 6, 24 April 2023

Observational Type Theory meets CIC slides video

Joint work with Nicolas Tabareau

HoTTEST Seminar, 23 February 2023

Extensionality in Intensional Type Theory slides

Joint work with Nicolas Tabareau

Rencontres Chocola, 10 March 2022

Computing with Univalence in Coq using Intensional Presheaves abstract slides

Joint work with Maxime Lucas, Pierre-Marie Pédrot, and Nicolas Tabareau

ICMS 2020

Synthetic homotopy theory in cubical type theory and the Hopf fibration

CMU HoTT seminar, 28 February 2019

Beyond the probability of coprimality slides

UTokyo, JFLI Internship Day, 20 July 2017

Notes and drafts

An inductive universe for setoids PDF Formalisation

Extended abstract presented at TYPES 2025

A semantic account of the presheaf translation PDF

Last update: 02/12/2020

Software

Observational Coq Github

Fork of Coq/Rocq with a modified kernel that supports OTT