Loïc Pujet

I am a postdoc in the department of mathematics of the University of Stockholm. Here is a picture of me.
My research interests lie mainly in type theory, proof assistants, homotopy theory and constructive mathematics.

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

News

12/06/2023 – Kenji Maillard gave a talk at TYPES 2023 on joint work with Arthur Adjedj, Meven Lennon-Bertrand, Kenji Maillard and myself. You can find the extended abstract here.
07/06/2023 – I was awarded a scholarship from the Sverker Lerheden foundation to conduct postoctoral studies at the University of Stockholm for two years.
24/04/2023 – I was invited to speak at Europroofnet Working Group 6. The slides are available here.
17/03/2023 – I gave a talk at the Boston University POPV seminar.
23/02/2023 – I gave a presentation at the HoTTEST seminar. The video is available on Youtube.

Research

Publications

Impredicative Observational Equality HAL slides

Loïc Pujet, Nicolas Tabareau

POPL 2023

Observational Equality: Now For Good HAL slides video

Loïc Pujet, Nicolas Tabareau

POPL 2022 (distinguished paper)

Cubical Synthetic Homotopy Theory HAL slides

Anders Mörtberg, Loïc Pujet

CPP 2020

PhD thesis

Computing with Extensionality Principles in Type Theory Github slides

PhD thesis, Nantes University, 2022

The version on Github should receive some minor corrections, but the contents are mostly final.

Talks

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

A semantic account of the presheaf translation PDF

Last update: 02/12/2020