Speaker / Predavač :
Prof. Pierre-Louis Curien
PPS Laboratory, pi.r2 team, CNRS, University Paris Diderot, and INRIA, France
Title / Naslov:
Curry-Howard isomorphism, sequent calculus, abstract machines, and classical logic
Abstract / Sažetak:
In this introductory talk, I shall review the correspondence between programs and proofs, given by a common formal language, the lambda-calculus (that was also the first formalism introduced about 80 years ago to formalise the notion of computable function). Lambda-calculus is both the basis of some programming languages like CAML or Haskell, and a notation to describe formal proofs in intuitionnistic logic and as such is the basis of some proof assistants, among which Coq has gained a lot of attention in recent years.
Formal proofs can be written in different styles. Lambda-calculus corresponds to a style called natural deduction. Another style, called sequent calculus, plays a crucial role as a foundation of logic programming. I shall introduce system L (based on works of Herbelin, Munch, and myself) that plays for (classical) sequent calculus the same role as lambda-calculus for natural deduction. System L gives a neat account of abstract machines for the execution of programs (giving a first-class status to the environment in which a program is executed). Finally, time permitting, we’ll see how Curry-Howard can be extended to classical logic, whose Curry-Howard counterpart is functional programming extended with control operators (or exceptions).