Talks

☰

1. A Realisability Model for Impredicative Linear Dependent Type Theory, talk at CT seminar in Utrecht.
2. A General Construction of Strict Models in HoTT, talk at TYPES2026, Gothenburg.
3. A realisability model of linear dependent type theory, talk at DutchCATs, Delft.
4. A realisability model of linear dependent type theory, talk at Formath Seminar, Paris.
5. Impredicativity in Linear Dependent Type Theory, talk at LIX seminar, Paris.
6. Inductive Types, lecture for the course Logical Verification, Amsterdam.
7. The UniMath Rocq Library, talk at EuroProofNet Workshop on Proof Libraries, Orsay.
8. Impredicative Encodings of Inductive and Coinductive Types, talk at FSCD2025, Birmingham.
9. The internal languages of univalent categories, talk at LICS2025, Singapore.
10. Impredicative Encodings of Inductive and Coinductive Types, talk at TYPES2025, Glasgow (video).
11. Impredicative Encodings of Inductive and Coinductive Types, talk at DutchCATs.
12. The Univalence Maxim and Univalent Double Categories, talk at CT seminar in Utrecht.
13. Insights From Univalent Foundations: A Case Study Using Double Categories, talk at CSL2025, Amsterdam.
14. How to give a talk, Logic Mentoring Workshop 2025, Amsterdam.
15. The internal languages of univalent categories, talk at CT seminar in Utrecht.
16. The internal languages of univalent categories, talk at HoTTEST2024 (video).
17. Univalent Enriched Categories and the Enriched Rezk Completion, talk at FSCD2024, Tallinn.
18. The Univalence Maxim and Univalent Double Categories, talk at TYPES2024, Copenhagen.
19. The Internal Language of Univalent Categories, talk at TYPES2024, Copenhagen.
20. The Interval Domain in Homotopy Type Theory, talk at Geuversfest.
21. Formalizing Double Categories in UniMath, talk at the CoREACT Seminar.
22. The Internal Language of Univalent Categories, talk at the Programming Languages Seminar in Delft.
23. Certifying higher-order polynomial interpretations, talk at rewriting/logic seminar.
24. Displayed Monoidal Categories for the Semantics of Linear Logic, talk at SWS seminar.
25. Displayed Monoidal Categories for the Semantics of Linear Logic, talk at CPP 2024, London, UK (video).
26. The Formal Theory of Monads, Univalently, talk at FSCD 2023, Rome, Italy.
27. Enriched Categories in Univalent Foundations, talk at TYPES 2023, Valencia, Spain (video).
28. Enriched Categories in Univalent Foundations, talk at HoTT/UF 2023, Vienna, Austria.
29. Category Theory in UniMath, talk at UniMath School III 2022, Cortona, Italy.
30. Semantics for two-dimensional type theory, talk at TYPES2022, Nantes (video).
31. Semantics for two-dimensional type theory, talk at Syntax and Semantics of Type Theories, Stockholm.
32. Constructing Higher Inductive Types as Groupoid Quotients, talk at LICS2020 (video, Q&A).
33. Constructing 1-truncated finitary higher inductive types as groupoid quotients, talk at HoTTEST2020 (video).
34. The Construction of Set-Truncated Higher Inductive Types, talk at MFPS. London.
35. Bicategories in Univalent Foundations, talk at FSCD2019, Dortmund.
36. Bicategories in Univalent Foundations, talk at TYPES2019, Oslo.
37. Category Theory in UniMath, talk at UniMath School II 2019, Birmingham.
38. Bicategories in Homotopy Type Theory, talk at EUTYPES meeting in Aarhus.
39. 1-Types vs Groupoids, talk at TYPES2018, Braga.
40. Finite Sets in HoTT, talk at EUTYPES meeting in Nijmegen.
41. Higher Inductive Types in Programming, talk at Agda Implementors Meeting XXVII, Gothenburg.
42. The Three-HITs Theorem, talk at FPFM workshop, Nantes.
43. Programming with Higher Inductive Types, talk at EUTYPES meeting, Ljubljana.
44. Higher Inductive Types, talk at HoTT/UF 2016, Porto.