User Tools

Site Tools

See veebisait esitab teavet KübIst 31. detsembri 2016 seisuga ja seda enam ei uuendata.
This website presents information about IoC as of 31 December 2016 and is no longer updated.

CS Theory Seminars

Duality in sequent calculus and abstract machines

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.

en/teated/2013/herbelin.txt · Last modified: 2013/10/02 11:46 by

© Institute of Cybernetics at TUT, Akadeemia tee 21, 12618 Tallinn, Estonia Phone: +372 620 4150 Fax: + 372 620 4151