Signatures and models for syntax and operational semantics in the presence of variable binding
2nd December 2019
Myself
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
Internships
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
My github profile
Commutative diagram editor
A commutative diagram editor in your browser
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.Initial semantics for substitution skew-monoids
A formalisation of Fiore-Plotkin-Turi Abstract Syntax and Variable binding in the setting of skew-monoidal categories.
ii-from-i
Constructing inductive-inductive datatypes from indexed inductive datatypes
weak-omega-coq
Weak omega groupoids/categories in Coq
weak-omega-agda
Weak omega groupoids in Agda
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
Generic pattern unification
Ambroise Lafont, Neel Krishnaswami
Preprint (2023)
A more general categorical framework for congruence of applicative bisimilarity
Tom Hirschowitz, Ambroise Lafont
Preprint (2023)
Dargent: A Silver Bullet for Verified Data Layout Refinement
Zilin Chen, Ambroise Lafont, Liam O'Connor, Gabriele Keller, Craig McLaughlin, Vincent Jackson, Christine Rizkallah
POPL 2023
A unified treatment of structural definitions on syntax for capture-avoiding substitution, context application, named substitution, partial differentiation, and so on
Tom Hirschowitz, Ambroise Lafont
Preprint (2022)
Variable binding and substitution for (nameless) dummies
André Hirschowitz, Tom Hirschowitz, Ambroise Lafont, Marco Maggesi
FoSSaCS 2022
A categorical framework for congruence of applicative bisimilarity in higher-order languages
Tom Hirschowitz, Ambroise Lafont
LMCS 2022
A Cellular Howe Theorem
Peio Borthelle, Tom Hirschowitz, Ambroise Lafont
LICS 2020
Modules over Monads and Operational Semantics
André Hirschowitz, Tom Hirschowitz, Ambroise Lafont
FSCD 2020, LMCS 2022
Reduction Monads and Their Signatures
Benedikt Ahrens, André Hirschowitz, Ambroise Lafont, Marco Maggesi
POPL 2020
For finitary induction-induction, induction is enough
Ambrus Kaposi, András Kovács, Ambroise Lafont
TYPES 2019 post-proceedings
Modular specification of monads through higher-order presentations
Benedikt Ahrens, André Hirschowitz, Ambroise Lafont, Marco Maggesi
FSCD 2019
Presentable signatures and initial semantics
Benedikt Ahrens, André Hirschowitz, Ambroise Lafont, Marco Maggesi
CSL 2018, LMCS 2021
Probing wave function collapse models with a classically driven mechanical oscillator
Melvyn Ho, Ambroise Lafont, Nicolas Sangouard and Pavel Sekatski (2018)
Other talks
A categorical diagram editor to help formalising commutation proofs
GReTA-ExACT seminar, 18 March 2022
Quantum oddities
CSE Seminar at UNSW, 10 November 2020
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
Higher-order Arities, Signatures and Equations via Modules
Chocola seminar (ENS Lyon) March 2019
Types are weak omega-groupoids, in Coq
Ambroise Lafont, Nicolas Tabareau and Tom Hirschowitz
TYPES 2018