Abstract
Martin Escardo is well-known for his many contributions to mathematics and computer science. One of them is his analysis of “seemingly impossible functional programs” (see e.g. “Infinite sets that admit fast exhaustive search”, Lics 2007). In his joint work with Paulo Oliva, he applied these types of programs to an amazing variety of areas such as sequential games, computable analysis, topology and logic (see e.g. “What Sequential Games, the Tychonoff Theorem and the Double-Negation Shift have in Common”, MSFP 2010).
In this talk I discuss another program, that has some similarity with Escardo/Oliva search, and that uses - somewhat surprisingly - a non-strictly positive inductive type to performs breadth-first search in a tree. The program goes back to Martin Hofmann (‘Non strictly positive datatypes in system F’, http://www.seas.upenn.edu/~sweirich/types/archive/1993/) and has been analysed from a type-theoretic and logical perspective (Ralph Matthes, Anton Setzer, B: “Martin Hofmann’s case for non-strictly positive data types”, TYPES 2018 post-proceedings, LIPIcs 130).
Talk Details
Speaker: Ulrich Berger (Swansea University, UK)
Event: Types and Topology Workshop in Honour of Martin Escardo’s 60th Birthday
Date: Wednesday 17 December 2025
Time: 15:30
Slides: Available
Key Topics
- Non-strictly positive inductive types
- Breadth-first search
- Tree algorithms
- Seemingly impossible functional programs
- System F
- Type theory
- Exhaustive search algorithms
Related Work
- Paulo Oliva - Higher-order game theory
- Martin Escardo’s “Infinite sets that admit fast exhaustive search” (LICS 2007)
- “What Sequential Games, the Tychonoff Theorem and the Double-Negation Shift have in Common” (MSFP 2010)
- Martin Hofmann’s “Non strictly positive datatypes in system F”
- Ralph Matthes, Anton Setzer, Berger: “Martin Hofmann’s case for non-strictly positive data types” (TYPES 2018)
Historical Context
This work builds on Martin Hofmann’s original exploration of non-strictly positive datatypes and connects to Escardo’s broader program of analyzing “seemingly impossible functional programs” and their applications across mathematics and computer science.