Josselin Poiret
About me
I am a mathematician by training, trying to wrap my head around higher algebra and higher algebraic geometry in particular. To help me along the way, I've found the approach of synthetic mathematics to be incredibly insightful, and thus am also working at the intersection of dependent type theories, proof assistants and their semantics. I am also interested in reducing the friction between formal and informal mathematical practice, by finding the right language for each job.
In my free time, I like to contribute (as well as use!) free software projects, mostly the GNU Guix distribution and things adjacent to it, such as GNU Guile.
What I've been up to
- March — July 2023: At Chalmers with Felix Cherubini, working on synthetic algebraic geometry. There is formalization work going on here.
- October 2022 — February 2023: At KU Leuven with Dominique Devriese and Andreas Nuyts, working on modal type theory. With other people met at the Agda Implementers Meeting, we've been trying to add explicit polarity annotations to Agda, see here for more.