Selected Research Talks
Various approaches to computing moduli of continuity (slides). Lecture at the Proof and Computation autumn school, Fischbachau, September 2022.
A certified library of ordinal arithmetic (slides, Agda-html). Continuity, Computability, Constructivity (CCC), Birmingham/online, September 2021.
Connecting constructive notions of ordinals in Homotopy Type Theory (slides). New Frontiers in Proofs and Computation, Hangzhou/online, September 2021.
Various structures of T-definable functionals via a Gentzen-style translation (slides). Mathematical Logic and Constructivity, Stockholm, August 2019.
Ordinal notations via simultaneous definitions (slides). ABM Spring 2019, Munich, May 2019.
A syntactic approach to continuity of Gödel's system T definable functionals (slides). Continuity, Computability, Constructivity (CCC), Faro, September 2018.
Unifying functional interpretations of nonstandard/uniform arithmetic (slides). Logic Colloquium 2018, Udine, July 2018.
A univalent approach to constructive mathematics (slides). Mathematical Logic and its Applications, Kanazawa, March 2018.
Using function extensionality in Agda, (non-)computationally (slides). Oberseminar Mathematische Logik, LMU Munich, December 2017.
Unifying (Herbrand) functional interpretations of (Nonstandard) arithmetic (slides). Proof and Computation, Verona, October 2017.
Extracting Computer Programs from Nonstandard Proofs (slides). Logic and its Applications, Mathematics Institute LMU, October 2016.
Sheaf models of type theory in type theory (slides). Mathematics for Computation (M4C), Niederalteich, Germany, May 2016.
A constructive manifestation of the Kleene-Kreisel continuous functionals (slides). Arbeitstagung Bern-München (ABM), Mathematics Institute LMU, December 2015.
When is the Kleene–Kreisel hierarchy full? (slides). Math Lunch talk in School of Computer Science, the University of Birmingham, November 2013.
A constructive model of unform continuity (slides). Typed Lambda Calculi and Applications (TLCA'2013), Eindhoven, the Netherlands, June 2013.
A constructive model of unform continuity (slides). Fourth Workshop on Formal Topology (4WFTop), Ljubljana, June 2012.
Last modified: Sat 1 October 2022