The Presheaf Model of Type Theory in Type Theory. 3-month intership supervised by Anders
Mörtberg at Stockholm University, during my M1. Report, Slides
Hashing and boolean decision trees in Rocq. 6-week internship supervised by David
Monniaux, at Université Grenobles-Alpes, during my L3. Report.