Ambroise Lafont


I am currently a postdoc in the Cogent team in Sydney. Before, I was a PhD student the Inria team Gallinette at LS2N in Nantes, supervised by Nicolas Tabareau and Tom Hirschowitz.

My research interests mainly lie in Type Theory and Category Theory.

The source code of this page is almost completely copied and pasted from Théo's personal page.

You can contact me at .

PhD manuscript

Formal verification of a JIT compiler for Coq

with Xavier Leroy, at INRIA Paris

April 2016 — August 2016

Probing wave function collapse models with a classically driven mechanical oscillator

with Nicolas Sangouard at University of Basel

Januar 2015 — March 2015

Publications and preprints

Other talks

Mathematical specifications of programming languages via modules over monads

Seminar LoVe at LIPN Paris 13, 29 October 2020

Seminar PPS at IRIF Paris 7, 26 November 2020



Constructing inductive-inductive datatypes from indexed inductive datatypes