Observational Equality meets CIC HAL slides Formalisation
Loïc Pujet, Nicolas Tabareau
ESOP 2024
I am a postdoc in the department of mathematics of the University of Stockholm, funded by the Sverker-Lerheden foundation.
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! .
Observational Equality meets CIC HAL slides Formalisation
Loïc Pujet, Nicolas Tabareau
ESOP 2024
Martin-Löf à la Coq HAL Formalisation
Arthur Adjedj, Meven Lennon-Bertrand, Kenji Maillard, Pierre-Marie Pédrot, Loïc Pujet
CPP 2024 (distinguished paper)
Impredicative Observational Equality HAL slides Formalisation
Loïc Pujet, Nicolas Tabareau
POPL 2023
Observational Equality: Now For Good HAL slides Formalisation
Loïc Pujet, Nicolas Tabareau
POPL 2022 (distinguished paper)
Cubical Synthetic Homotopy Theory HAL slides
Anders Mörtberg, Loïc Pujet
CPP 2020
Computing with Extensionality Principles in Type Theory Github slides
PhD thesis, Nantes University, 2022
The version on Github is the finished product, I am waiting for the university to put it on a more official-looking platform...
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
A semantic account of the presheaf translation PDF
Last update: 02/12/2020
Github - Mastodon - StackExchange