Writings

Notes

• Notes on Locally Cartesian Closed Categories [notes (src)]
• Notes on Grothendieck Fibrations [notes (src)|slides (src)]

Internship thesis

• Syntax and Semantics of a Linear Dependent Type Theory [thesis|slides]
• 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)]