## Duality in sequent calculus and abstract machines

Équipe πr^{2}

Preuves, Programmes et Systèmes (PPS)

INRIA Paris - Rocquencourt

Thursday, 3 October 2013, 11:00 (note the unusual time!)

Cybernetica Bldg (Akadeemia tee 21), room B101

**Abstract**: 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.

Tarmo Uustalu

Last update 1.10.2013