- Review of first order intuitionistic logic, Heyting arithmetic and higher order versions of Heyting arithmetic.
- Brouwerian omniscience principles
- Heyting valued models, topologies and formal topologies
- Separating omniscience principles, independence of countable choice
- Introduction to partial combinatory algebras and realizability
- Computable functions and the first Kleene algebra, Kleene realizability, consistency of Church's thesis (all functions are computable)
- The Kleene tree, non-compactness of Cantor space in Kleene realizability
- Baire space and the second Kleene algebra, function realizability, consistency of the Fan theorem and Brouwer's principle (all functions are continuous)
- Kleene and Aczel slash constructions, extracting witnesses of existential sentences, the numerical existence property and disjunction property
- q-realizability, another proof of the numerical existence property and disjunction property, Church's rule

- Introduction(revised 10/1/21)
- Heyting arithmetic(revised 9/8/21)
- Omniscience principles(revised 10/4/21)
- Heyting algebras and topology(revised 9/21/21)
- Heyting valued models(revised 10/4/21)
- Kripke models and formal topological models(revised 10/26/21)
- Heyting valued models of second order arithmetic(revised 10/5/21)
- Heyting valued models of arithmetic with finite types(revised 10/26/21)
- Independence of choice and omniscience principles over \(\mathbf{HA}_\omega\)(revised 10/26/21)
- Completeness and existence properties(revised 10/26/21)
- Partial combinatory algebras(revised 10/28/21)
- Realizability(revised 11/2/21)
- Kleene Realizability(revised 11/16/21)
- The second Kleene algebra and function realizability(updated 11/24/21)
- Realizability with truth

- Exercise sheet 1(updated 9/7/21) solutions
- Exercise sheet 2(updated 9/13/21) solutions
- Exercise sheet 3 solutions
- Exercise sheet 4(updated 9/28/21)
- Exercise sheet 5
- Exercise sheet 6
- Exercise sheet 7(updated 10/25/21)
- Exercise sheet 8
- Exercise sheet 9(updated 11/10/21)
- Exercise sheet 10

- McCarty, Realizability and Recursive Mathematics, PhD Thesis, Ohio State University
- Rathjen, Realizability for constructive Zermelo-Fraenkel set theory

- Lifschitz, \(\mathbf{CT}_0\) is stronger than \(\mathbf{CT}_0 !\)
- Van Oosten, Lifschitz' realizability

- Beeson, Goodman's theorem and beyond
- Chapter XV, section 2 of Beeson, Foundations of Constructive Mathematics
- Goodman, The theory of Gödel functionals
- Goodman, Relativized Realizability in Intuitionistic Arithmetic of All Finite Types

- Chapter 9, sections 4.9-4.14 of Troelstra, Van Dalen, Constructivism in Mathematics, Volume II
- Lietz, Streicher, Realizability models refuting Ishiharaʼs boundedness principle

- Grayson, Heyting valued models for intuitionistic set theory
- Gambino, Heyting-valued interpretations for Constructive Set Theory

- Chapter 14 of Troelstra, Van Dalen, Constructivism in Mathematics, Volume II
- Fourman, Scott, Sheaves and logic

- Hyland, The effective topos, The L.E.J. Brouwer Centenary Symposium
- Van Oosten, Realizability: An introduction to its categorical side

Troelstra, Van Dalen, Constructivism in Mathematics, Volume II