This repository contains a draft of notes on realizability theory in the notes folder. You may download a recent PDF version of the notes.
The folder reading contains classic historical papers and other useful publications about realizability.
The notes are the main reading material for the Midlands Graduate School 2022 lecture series on realizability.
Time: Sunday, April 10, 2022, 14:00–15:00
Contents:
- some models of computation
- partial combinatory algebras
- assemblies
Reading material: The chapter “Models of computation” from the notes.
Exercises: (Monday, April 11, 2022, 10:30–11:25) Consult “Lecture 1” of the exercise sheet.
Time: Monday, April 11, 2022, 14:00–15:00
Contents:
- modest assemblies
- equivalent formulations
- examples of assemblies
- the categorical structure of assemblies
Reading material: The chapter “Realiability categories” from the notes.
Exercises: (Tuesday, April 12, 2022, 10:30–11:25) Consult “Lecture 2” of the exercise sheet.
Time: Tuesday, April 12, 2022, 14:00–15:00
Contents:
- families of assemblies
- products and sums of assemblies
- propositions as assemblies
- the identity type
- universes of assemblies
Reading material: The chapter “Realiability and type theory” from the notes. Disclaimer: this chapter is not complete yet.
Exercises: (Wednesday, April 13, 2022, 10:30–11:25) Consult “Lecture 3” of the exercise sheet.
Time: Wednesday, April 13, 2022, 14:00–15:00
Contents:
- realizability logic
- the axiom of choice
- countable objects
- Church's thesis
- continuity principles
Reading material: The chapter “The internal language at work” from the notes. Disclaimer: this chapter is not written yet, but at least lecture notes will be published before the lecture.
Exercises: (Wednesday, April 13, 2022, 17:00–17:55) Consult “Lecture 4” of the exercise sheet.