2026 MFPS'XLII . An inductive-recursive universe of searchable ordinals.
2026 7WFTop . Stone Types.
2025 ASSUME. Taking "algebraically" seriously in the definition of algebraically injective type.
2025 HoTTEST seminar. Injective types
2024 LICS2024. Topology in constructive mathematics and computation.
2023 CIRM2023. Compact ordinals in HoTT/UF.
2023 encontro-games. Playing rationally against irrational players using monads.
2022 totally-separated. Totally separated types.
2022 large-group. There are more groups in the next universe.
2022 ljubljana2022. Searchable types in HoTT/UF.
2022 topos2022. Compact totally separated types in univalent mathematics.
2022 csl2022. Seemingly impossible programs and proofs.
2021 YaMCATS. Equality of mathematical structures.
2020 UWLS. Equality of mathematical structures.
2019 universe-oddities. Universe oddities.
2019 ccc2019. Equality of mathematical structures.
2019 xii-pcc. Equality of mathematical structures.
2019 compact-ordinals. Compact totally separated and well ordered types in univalent mathematics.
2019 Compact-Types-2019. Compact totally separated and well ordered types in univalent mathematics.
2018 injective-types. Injective types in univalent mathematics.
2017 prague2017. The frame of Scott continuous nuclei on a preframe.
2017 univalent-logic. Logic in univalent type theory.
2016 leeds2016. On the versatile selection monad with applications to proof theory.
2016 bath-2016. Continuity in constructive dependent type theory.
2016 porto2016. Compact types and ordinals in constructive univalent type theory.
2016 5wft. Continuity in constructive dependent type theory.
2016 tlca2015. Continuity in constructive dependent type theory.
2016 stockholm2016. When the principle of omniscience just holds.
2015 HoTT-UF-2015. The geometry of constancy (in HoTT and in cubicaltt) (and cubicaltt file).
2015 ccc2015. Infinite, exhaustibly searchable sets in dependent type theory and everywhere.
2015 masterclass.lhs. Computing with numbers coded as finite lists of digits.
2014 domains2014. The topology of the universe and related continuity phenomena in Martin-L¨of Type Theory.
2014 cca-2014. A constructive manifestation of the Kleene-Kreisel continuous functionals.
2014 psc2014. Excluded middle considered as a mathematical problem.
2014 ihp2014. Continuity in type theory.
2013 mfps2013. Continuity of G¨odel’s system T functionals via eﬀectful forcing.
2013 phdopen2013. Topological ideas in computation.
2013 scotcat2013. Sheaves in type theory: a model of uniform continuity.
2012 4WFT. The intrinsic topology of a univalent universe.
2012 DCM2012. The intrinsic topology of a universe in intuitionistic type theory.
2012 mfps2012. The topology of the universe.
2012 mgs2012. Computing with infinite objects.
2012 EWSCS2012. Topology for functional programming.
2012 popl2012. the topology of seemingly impossible programs.
2011 map2011. Categorical axioms for functional real-number computation.
2011 invariant-2011. Mathematics of computation with infinite objects.
2011 dagstuhl2011. Infinite sets that satisfy the principle of omniscience in all varieties of constructive mathematics.
2011 wessex2011-queen-mary. Infinite sets that satisfy the principle of omniscience in all varieties of constructive mathematics.
2011 wessex2011-swansea. The ubiquitous selection monad.
2011 types2011. Infinite sets that satisfy the principle of omniscience in all varieties of constructive mathematics.
2011 imperial2011. An amazingly versatile functional.
2011 mfps2011. Programs from proofs.
2011 mgs2011. Game Theory, Topology and Proof Theory for Functional Programming.
2011 leeds2011. When is universal quantification decidable?
2011 cambridge2011. Selection functions everywhere.
2010 mfps2010. Topology, computation, monads, games and proofs.
2010 msfp2010. What Sequential Games, the Tychonoﬀ Theorem and the Double-Negation Shift have in Common.
2010 clp2010. Maybe locales are made of points after all.
2010 lablunch-birmingham. Searchable sets, Dubuc-Penon compactness, Omniscience Principles, and the Drinker Paradox.
2009 cie2009. Computability of continuous solutions of higher-type equations.
2009 mgs2009. Semantics for the lazy functional programmer.
2009 mfps2009. Semi-decidability of may, must and probabilistic testing in a higher-type setting.
2008 mgs2008. Domain theory and denotational semantics of functional programming.
2004 dagstuhl2004. A Hausdorff compactification of the Samborski function space.
2002 dagstuhl2002. Applications of the lambda-calculus to topology.
2000 issac. Exact numerical computation.