Talks
2026
A canonical normal form theorem for the type theory of regular categories
SSTT 2026, Ljubljana, Slovenia, co-located with MFPS 2026, 4-5 June 2026. Slides.
Kraus’s Magic Trick for Computing with Constructive Reals
PACM∧N 2026, Verona, Italy, 10-12 June 2026. Joint work with Lorenzo Molena and Marcin Jan Turek-Grzybowski. Slides.
Where does ACω hide in constructive reals?
Dagstuhl Seminar 26121, “Proof Systems in Actual Practice: Reasoning and Computation”, Schloss Dagstuhl, Germany, 16 March 2026. Slides.
2025
NAMOR: a New Agda Library for Modal Extended Sequents
OVERLAY 2025, Bologna, Italy, 26 October 2025. With Margherita Zorzi. Slides.
An Agda Implementation of the Modal Logic S4.2: First Investigations
ICTCS 2025, Pescara, Italy, 12 September 2025. With Margherita Zorzi. Slides.