Modern game semantics grew out of the full completeness problem for linear logic and the full abstraction problem for PCF, and more recently it has been applied to the study of type systems and programming languages. My past work took a new direction by developing game semantics into a model of higher-order computation and a foundation of maths. Concretely, my games form a categorical foundation of constructive maths, and it captures (un)computability/complexity at any higher type for the first time. This game-semantic approach has compelling conceptual naturality, overcomes the syntactic nature of foundations of maths and defines (un)computability/complexity of any mathematical objects and proofs. On the other hand, Henri Poincaré famously declared that point set topology is a disease from which the human race will soon recover. To address the problems of point set topology, I have recently constructed a new foundation of topology in terms of groupoids internal to the category of games. The intuition here is that topology is the study of computational equality/nearness, and invertible morphisms in groupoids witness the computational equality/nearness. This approach not only solves the problem of point set topology but also conceptually makes sense. This construction is carried out at the general level of category theory, and in essence it is an internal quotient. From the categorical viewpoint, this quotient endows the category of games with the extensional structure of a predicative variant of topoi such as all (co)limits, while it preserves the flagship intensional structure of games for (un)computability/complexity. In this talk, I present an overview of this line of work and propose further directions.
|