Swansea University
Computer Science

Seminar series on realizability theory

Next meeting

No more meetings.

Realizability was introduced by Kleene in 1945. It is a model that is understandable by people used to classical logic, but it satisfies the rules of constructive logic, thus serving as a concrete reason to study constructive logic. Realizability can model all the hereditary effective operations on higher type, this is known as the effective topos. The effective topos carries a uniform notion of truth for higher type objects. In another direction, realizability contains information about the computational content of formulae, and can hence be used to extract programs from logical proofs.

Time and place

15.00 – 16.00 in the Small Talk room.

Prerequisites

It will be helpful to know some basic recursion theory, but in general very little is assumed. We aim to keep the seminar friendly.

Literature

We will follow all or parts of the following literature:

Supplemental reading

Time plan

10/10 0. Overview of realizability. Uli
17/10 0½. Prerequisites recursion theory [Chapter 8 in Intro to Constructive Mathematics] Matt
24/10 0½. Exercises on recursion theory
31/10 1. Kleene's number realizability [Chapter 9 in Intro to Constructive Mathematics] Stewart
7/11 1½. Exercises on number realizability Stewart
14/11 2. Kleene's function realizability Phil
21/11 2½. Exercises on function realizability Phil
28/11 3. Modified realizability [Chapters 12 and 13 in Intro to Constructive Mathematics] Greg
5/12 3½. Modified realizability II Greg
12/12 3¾. Exercises on modified realizability Greg
– Christmas –
6/2 4. Program extraction Andy
13/2 5. My summer in Munich Fred
20/2 6. Partial Combinatory Algebras
[Section 3 in Realizability (Streicher), Sections 1.1–1.4 in Realizability (van Oosten)]
Caroline
27/2 6½. Examples/questions session on PCAs Caroline
6/3 7. The category of assemblies
[Section 1.5 in Realizability (van Oosten)]
Jens
13/3 7½. The category of assemblies II Jens
20/3 7¾. Exercises on assemblies Jens
– Easter –
17/4 8. Canonical Effective Subalgebras of Classical Algebras as Constructive Metric Completions Jens
24/4 8.½ Canonical Effective Subalgebras of Classical Algebras as Constructive Metric Completions II Jens
1/5 8.¾ Canonical Effective Subalgebras of Classical Algebras as Constructive Metric Completions III Jens

Fredrik Nordvall Forsberg. Last modified: Wed 1 May 16:13:45 UTC 2013.