Extracting programs from classical proofs

Lecturer: Prof. Thierry Joly (Universite Paris VII Denis Diderot, France).

About the lecturer | Abstract | Slides | Assignment (NEW DEADLINE!!)

About the lecturer: Thierry Joly belongs to the younger generation of researchers in the area of type theory and lambda-calculus. He received his PhD in 2000, then worked at the Catholic University of Nijmegen and lectured at I.U.T. (Institut Universitaire de Technologie) of Villetaneuse. Presently he is a Maître de conférence at Universite Paris VII.
Thierry Joly is known for a series of hard results on the definability problem in finite types. In particular he has shown that the definability problem is decidable for a type iff and only if it is finitely generated.

Course summary: The mini-course will be an introduction to the subject. We will first recall the lambda-realizability (i.e. realizability by lambda-terms) of the intuitionistic logic and stress a few basic ideas about it: How Hilbert style axiomatic presentations of the deduction system correspond to combinatoric presentations of the calculus. How the usual formulae-as-types realizability splits into a logical relativisation (that can be viewed as a task of preprocessing) and a lighter realizability defined as in [1]... The lambda-realizability of the intuitionistic logic then will be extended to the classical logic in a similar way as in [2]. The classical lambda-calculus considered will borrow the fewest as possible from Herbelin's $\overline{\lambda}\mu\tilde{\mu}$-calculus in order to contain both Parigot's lambda-mu-calculus and Krivine's lambda-cc-calculus.
References:
[1] J.-L. Krivine. Lambda-calculus, types and models. Ellis Horwood, 1993. [PDF]
[2] J.-L. Krivine. Realizability in classical logic, 2004. [PDF]

Assignment mixed with lecture slides [PDF] due January 31 (MOVED!!), 2008.
Solutions should be sent in one one following ways: