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.


Invited speakers


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:


Submission of abstracts on published work is allowed.

  • Deadline for talk proposals: December 15th 2011