TTÜ Küberneetika Instituut

Hugo Herbelin

INRIA, Rocquencourt-Paris

Thursday, 3 October 2013, 11:00
Cybernetica Bldg (Akadeemia tee 21), room B 101

The proofs-as-programs correspondence, in its strictly syntactic formulation, connects intuitionistic Hilbert-style axiomatic logic to combinatory logic and Gentzen's intuitionistic natural deduction to lambda-calculus. This connection extends to classical logic, by considering e.g. Parigot's mu operator or Scheme's call-cc operator.

Sequent calculus is a symmetric deductive system for classical logic that Gentzen used to prove the consistency of arithmetic. In sequent calculus, the only computation rule is the cut rule and this happens to be connected to abstract machines.

We will review these connections and in particular introduce the mu-mu-tilde-calculus, which is at the core of sequent calculus and abstract machines. There is an inherent critical pair in the mu-mu-tilde calculus and we will show that depending on how the critical pair is resolved, one obtains call-by-name, call-by-value, or even call-by-need evaluation theories.