Notes Notes on Locally Cartesian Closed Categories [notes (src)] Notes on Grothendieck Fibrations [notes (src)|slides (src)] Internship thesis Two-level Type Thoery in Lean, and Applications to Semi-Simplicial Type in HoTT [thesis|slides] Approximate Streaming Regular Pattern Matching [thesis|slides] Automatic Benchmark Generation [thesis|slides (in French)]