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

- In PDF by e-mail to joly AT pps.jussieu.fr (scanned handwritten versions in order to avoid typewriting proof trees are welcome)
- by snail-mail to:

Thierry Joly

Laboratoire PPS

Universit Paris Diderot - Paris 7

Case 7014

75205 PARIS Cedex 13

FRANCE