Call-by-value is Dual to Call-by-name

The paper

  Call-by-value is Dual to Call-by-name
  Philip Wadler, ICFP 2003, Uppsala, Sweden, 25-29 August 2003.

is available at


Comments welcome!  -- P


The rules of classical logic may be formulated in pairs corresponding
to De Morgan duals: rules about & are dual to rules about \/. A line
of work, including that of Filinski (1989), Griffin (1990), Parigot
(1992), Danos, Joinet, and Schellinx (1995), Selinger (1998,2001), and
Curien and Herbelin (2000), has led to the startling conclusion that
call-by-value is the de Morgan dual of call-by-name.

This paper presents a dual calculus that corresponds to the classical
sequent calculus of Gentzen (1935) in the same way that the lambda
calculus of Church (1932,1940) corresponds to the intuitionistic
natural deduction of Gentzen (1935). The paper includes crisp
formulations of call-by-value and call-by-name that are obviously
dual; no similar formulations appear in the literature. The paper
gives a CPS translation and its inverse, and shows that the
translation is both sound and complete, strengthening a result of
Curien and Herbelin (2000).

Philip Wadler wadler@avaya.com 
Avaya Labs, 233 Mount Airy Road, Basking Ridge, NJ 07920 USA
phone +1 908 696 5137 fax +1 908 696 5402 mobile +1 908 656 4518
"When a Mathematical Reasoning can be had it's as great a folly
to make use of any other, as to grope for a thing in the dark,
when you have a Candle standing by you." John Arbuthnot, 1692