Ambroise Lafont

Myself

I am an assistant professor at Ecole Polytechnique in the PARTOUT team since October 2023.

My research interests mainly lie in Type Theory and Category Theory, see my research statement. My email address is .

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

Software Projects

Cogent

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.

ii-from-i

Constructing inductive-inductive datatypes from indexed inductive datatypes

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