Proofs and programs (13 – 17 February)
The theme of this week is the correspondence between mathematical proofs and computer programs, known as the Curry-Howard correspondence. It notably includes the latest developments the theory of realizability, which can give computational content to proofs in classical logic, so as to allow the extraction of effective programs from classical proofs. In contrast to the previous week (logic and interaction), this week will focus on the study of logical aspects of non-functional programming: delimited continuations, references, effects, etc.
Lecturers
- Hugo Herbelin (INRIA, Paris, France)
- Guy McCusker (Bath, UK)
- Alexandre Miquel (ENS Lyon, France)
- Gordon Plotkin (Edinburgh, UK)
Invited speakers
- Ulrich Berger (Swansea, UK)
- Peter Dybjer (Chalmers University)
- Paul-André Melliès (CNRS, Paris, France)
- Thomas Streicher (Darmdstadt, Germany)
- Jaap van Oosten (Utrecht, Netherlands)
Programme
The mornings will be structured in tutorials. The afternoons are intended to be a space for the researchers to discuss recent developments and open issues. Both invited and contributed talks are planned.
Call for contributions
Abstract and title must be submitted electronically to the three organizers:
- olivier.laurent@ens-lyon.fr
- alexandre.miquel@ens-lyon.fr
- alexis.saurin@pps.jussieu.fr
Submission of abstracts on published work is allowed.
- Deadline for talk proposals: December 15th 2011