Ambroise Lafont


Since 2022, I am a postdoc in the TypeFoundry project in Cambridge. Previously, I was 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.

You can contact me at .

The layout of this website is based on a previous version of Theo Winterhalter personal page, which is also popular in its current form (see Anja Komel's personal page).

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

Software Projects


I worked on the Dargent extension, editing the Isabelle codebase mostly, and occasionally the compiler (written in Haskell). Dargent allows you to customise how Cogent types are laid out in memory when compiling to C. See the code on github.


Constructing inductive-inductive datatypes from indexed inductive datatypes

Teaching experience

See my research and teaching statement for more details.

During my PhD (2016-2019), I mostly taught to engineering students of IMT Atlantique.

  • Python, 30h tutoring (including designing the material) at the UCO University, 2018
  • Probability and statistics, 25h for students enrolled in an apprenticeship program at IMT Atlantique, 2018
  • Co-supervision of bachelor student projects, 20h tutoring at IMT Atlantique, 2018
  • Object-oriented programming in Java, 40h tutoring at IMT Atlantique, 2017
  • Haskell, 12h tutoring at IMT Atlantique, 2018
  • Linear programming, 7h tutoring at IMT Atlantique, 2018
  • Algorithmic structures, 16h tutoring at IMT Atlantique, 2017

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

Seminar Proofs and algorithms at LIX Palaiseau, 22 February 2021

Seminar LDP at I2M Marseilles, 29 April 2021