Lecture notes with exercises for the advanced course on Categorical Realizability at the Midlands Graduate School (MGS) 2024
Realizability, as invented by Kleene, is a technique for elucidating the computational content of mathematical proofs. In this course we study realizability from a categorical perspective. Starting from an abstract and general model of computation known as a partial combinatory algebra (pca), we construct the category of assemblies over it. Intuitively, an assembly is a set together with computability data and an assembly map is a function of sets that is computable. Here, the notion of computability is prescribed by the pca. Through the framework of categorical logic, the assemblies give rise to the realizability interpretation of logic, which we spell out in detail.
The central theme of this course is the interplay between category theory, logic and computability theory. While some familiarity with basic category theory (e.g. (co)limits and adjunctions) is required for some parts of the notes, the course hopefully offers plenty to those unfamiliar with category theory.
If you find an inaccuracy of any kind in the notes, then please help me fix it:
- If you know how to fix it and are comfortable using GitHub, please consider making a pull request with your fix.
- If you don't know how to fix it and are comfortable using GitHub, please consider creating an issue addressing the inaccuracy.
- If you don't wish to use GitHub, please inform me of the inaccuracy by
sending me an email at
tom.dejong[symbol]nottingham.ac.uk.
Your feedback is anonymous and will be used to improve future lectures.