Notes on realizability

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.

Midlands graduate school 2022

The notes are the main reading material for the Midlands Graduate School 2022 lecture series on realizability.

Lecture 1: Models of computation

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.

Lecture 2: Realizability categories

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.

Lecture 3: Realizability and type theory

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.

Lecture 4: The internal language at work

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.