
TypOS: An “Operating System” for Typechecking Actors.
TYPES 2022, June 2022, Nantes.
Slides Video


Different Notions of Ordinals in Homotopy Type Theory.
HOTTEST seminar, March 2022, online.
Slides Video


Functorial adapters.
TYPES 2021, June 2021, online.
Video


Constructive Notions of Ordinals in Homotopy Type Theory.
TYPES 2021, June 2021, online.
Slides Video


Quantitative Polynomial Functors.
Workshop on Polynomial Functors, March 2021, Topos Institute.
Slides Video


Ordinal notation systems for ordinals below ε_{0} in modern type theories.
LFCS seminar, February 2020, Edinburgh.
Slides


Compositional Game Theory in Type Theory.
TYPES 2019, June 2019, Oslo.
Slides


Specifying quotient inductiveinductive types.
TYPES 2018, June 2018, Braga.
Slides


Variations on inductiverecursive definitions.
Agda Implementors' Meeting XXV, May 2017, Gothenburg.
Slides


Comprehensive parametric polymorphism.
LFCS seminar, May 2016, Edinburgh.
Slides


The encodedecode method in HoTT, relationally.
Scottish Theorem Proving Seminar, October 2015, Dundee.
Slides


Inductiveinductive definitions in Intuitionistic Type Theory.
Stockholm Logic seminar, June 2014, Stockholm.
Slides


My Summer in Munich: Extracting Haskell Programs.
Realizability Seminar, February 2013, Swansea.
Slides


Internalising inductiveinductive definitions in MartinLöf Type Theory.
TCS Oberseminar, November 2012, LMU Institut für Informatik, Munich, Germany.
Slides


Elimination principles for initial dialgebras.
TYPES 2011, Bergen, Norway.
Slides


A categorical semantics for inductiveinductive definitions.
CALCO 2011, Winchester, UK.
Slides


Interpreting inductiveinductive definitions as indexed inductive definitions.
TYPES 2010, Warsaw, Poland.
Slides
