The duality of computation

We review the close relationship between abstract machines for (call-by-name or call-by-value) λ-calculi (extended with Felleisen’s C) and sequent calculus, reintroducing on the way Curien-Herbelin’s syntactic kit expressing the duality of computation. We use this kit to provide a term language for a presentation of LK (with conjunction, disjunction, and negation), and to transcribe cut elimination as (non confluent) rewriting. A key slogan here, which may appear here in print for the first time, is that commutative cut elimination rules are explicit substitution propagation rules. We then describe the focalised proof search discipline (in the classical setting), and narrow down the language and the rewriting rules to a confluent calculus (a variant of the second author’s focalising system L). We then define a game of patterns and counterpatterns, leading us to a fully focalised finitary syntax for tic presentation of classical logic, that provides a quotient on (focalised)...

• Type: Conference
• Year: 2000
• Where: ICFP
• Authors: Pierre-Louis Curien, Hugo Herbelin
• Keywords: Curien-Herbelin’s Syntactic Kit, Cut Elimination, Cut Elimination Rules, ICFP 2000, Programming Languages