Types and Topology
A workshop in honour of
Martin Escardo’s 60th birthday
17–18 December 2025
Co-located with the MGS Christmas Seminar on 16 December 2025.
About
Martín Escardó, professor in Theoretical Computer Science at the University of Birmingham, will turn 60 in November 2025. We are organizing a workshop to celebrate this occasion as well as Martín’s diverse contributions to constructive mathematics, domain theory, locale theory, logic, topology and homotopy/univalent type theory.
The workshop will take place in Birmingham on 17 and 18 December 2025 and is co-located with the MGS Christmas Seminar on 16 December 2025.
There will be a Zoom livestream for the workshop.
If you have slides, please send them to mhe60@proton.me some time ahead of your talk.
Venue
Lecture Theatre 2
Alan Walters Building
University of Birmingham
Birmingham B15 2SB, United Kingdom
Campus map
OpenStreetMap Google Maps Apple Maps
Programme
Wednesday 17 December 2025
Morning Session
- 08:55 Opening by Aad van Moorsel
- 09:00 Maria Emilia Maietti - On the compatibility of dependent type theory with Brouwer’s intuitionistic principles
- 09:25 Christopher Townsend - Escardo’s Patch
- 09:50 Ho Weng Kin - The Collatz Problem of domain theory Is FS = RB (recorded)
Late Morning
- 11:00 Thorsten Altenkirch - The reals as a higher coinductive type
- 11:25 Peter Dybjer - Are universes open or closed
- 11:50 Fredrik Nordvall Forsberg - Representing type theory in type theory with inspiration from natural models
Afternoon
- 13:45 Jon Sterling - What do mapping cylinders classify
- 14:10 Ulrik Buchholtz - Towards a synthetic mathematics of synthetic mathematics
Late Afternoon
- 15:05 Paulo Oliva - Higher-order game theory
- 15:30 Ulrich Berger - Non-strictly positive induction for breadth-first search
- 16:15 Gordon Plotkin - Using the selection monad (remote)
- 16:40 Giovanni Sambin - Informal address (remote)
19:00 Social dinner at Pasta di Piazza
Thursday 18 December 2025
Morning Session
- 09:30 Andrej Bauer - How to use excluded middle safely
- 09:55 Andrew Swan - The cohomology of the natural numbers in cubical assemblies
- 10:20 Hajime Ishihara - A constructive theory of uniformity and its application to integration theory (remote)
Late Morning
- 11:10 Alex Simpson - Martin’s interval in Scotland
- 11:35 Steve Vickers - Escardó-Simpson interval objects and point-free trigonometry
Afternoon
- 13:30 Thierry Coquand - Sheaf models of dependent type theory (remote)
- 13:55 Peter Schuster - Ultimate Glivenko
Late Afternoon
- 14:50 Dag Normann - Quantifiers in real analysis (remote)
- 15:15 Thomas Powell - Applications of proof theory in probability and stochastic optimization
- 16:00 Nicolai Kraus - From Hedberg’s theorem to truncation elimination and two-level type theory
- 16:25 Dan Christensen - Diagram chasing in the Coq-HoTT library (remote)
- 16:50 Closing
Thematic Groupings
Type Theory and Foundations
- Maria Emilia Maietti - On the compatibility of dependent type theory with Brouwer’s intuitionistic principles
- Peter Dybjer - Are universes open or closed
- Fredrik Nordvall Forsberg - Representing type theory in type theory with inspiration from natural models
- Nicolai Kraus - From Hedberg’s theorem to truncation elimination and two-level type theory
- Thierry Coquand - Sheaf models of dependent type theory
Topology and Analysis
- Christopher Townsend - Escardo’s Patch
- Alex Simpson - Martin’s interval in Scotland
- Steve Vickers - Escardó-Simpson interval objects and point-free trigonometry
- Thorsten Altenkirch - The reals as a higher coinductive type
- Hajime Ishihara - A constructive theory of uniformity and its application to integration theory
Domain Theory and Computability
- Ho Weng Kin - The Collatz Problem of domain theory Is FS = RB
- Andrew Swan - The cohomology of the natural numbers in cubical assemblies
- Dag Normann - Quantifiers in real analysis
Game Theory and Selection Functions
Logic and Proof Theory
- Andrej Bauer - How to use excluded middle safely
- Peter Schuster - Ultimate Glivenko
- Thomas Powell - Applications of proof theory in probability and stochastic optimization
- Dan Christensen - Diagram chasing in the Coq-HoTT library
Algorithms and Programming
- Ulrich Berger - Non-strictly positive induction for breadth-first search
- Jon Sterling - What do mapping cylinders classify
Synthetic Mathematics
Workshop Statistics
Total Talks: 24 (including informal address)
Remote Presentations: 6
Recorded Presentations: 1
Speakers with Slides Available: 13
Key Themes
The workshop showcases the breadth of Martin Escardo’s influence across multiple areas:
- Constructive mathematics and type theory
- Topology and analysis
- Domain theory and computability
- Game theory and optimization
- Logic and proof theory
- Synthetic mathematics approaches
The talks demonstrate ongoing collaborations and the continuing development of research areas that Escardo has contributed to or initiated throughout his career.
Local Information
For information on travel and accomodation, we kindly refer you to the local information page for FSCD 2025 which was also held in Birmingham.
Lunch options
On campus
- Campus map with food and drink options
- Cuore at the Green Heart
- Various food trucks along the Green Heart
Off campus (in Selly Oak)
- Woodstock (Chinese)
OpenStreetMap Google Maps Apple Maps - Kimchi (Korean)
OpenStreetMap Google Maps Apple Maps - Yakinori (Japanese)
OpenStreetMap Google Maps Apple Maps - The Goose (Pub)
OpenStreetMap Google Maps Apple Maps - Jaipur Lounge (Bangladeshi)
Google Maps Apple Maps
Organizers
- Eric Finster (University of Birmingham)
e.l.finster@bham.ac.uk - Tom de Jong (University of Nottingham)
tom.dejong@nottingham.ac.uk