# 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:

- Realizability by Thomas Streicher

(Lecture notes from Winter 2004/2005 - available here). - Introduction to Constructive Logic and Mathematics

(Lecture notes from Winter 2000/2001 - available here).

##### Supplemental reading

- van Oosten, J:
*Realizability: An introduction to its categorical side*, Studies in Logic and the Foundations of Mathematics, Elsevier, 2008. - Birkedal, E and Butz, C:
*Topos Theory Seminar*, Fall 2004, available here. - van Oosten, J:
*Realizability: a historical essay.*, Mathematical Structures in Computer Science, Volume 12, Issue 3, pages 239-263, Cambridge University Press. Available here. - Collection of links to recent papers on realizability and related topics: here.

### 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.