# Call-by-value is dual to call-by-name

## Philip Wadler

### Down with the bureaucracy of syntax!
Pattern matching for classical linear logic

Philip Wadler.
Draft.
This paper introduces a new way of attaching proof terms to proof
trees for classical linear logic, which bears a close resemblance to
the way that pattern matching is used in programming languages. It
equates the same proofs that are equated by proof nets, in the
formulation of proof nets introduced by Dominic Hughes and Rob van
Glabbeek; and goes beyond that formulation in handling exponentials
and units. It provides a symmetric treatment of all the
connectives, and may provide programmers with improved insight into
connectives such as ``par'' and ``why not'' that are difficult to treat in
programming languages based on an intuitionistic formulation of linear logic.

#### Paper available in:
pdf.

### Call-by-value is dual to call-by-name, reloaded

Philip Wadler.
Invited talk,
Rewriting Techniques and Applications (RTA),
Nara, April 2005.
We consider the relation of the dual calculus of Wadler (2003) to
the lambda-mu-calculus of Parigot (1992).
We give a translation from the lambda-mu-calculus into the
dual calculus, and an inverse translation from the dual calculus
back into the lambda-mu-calculus.
The translations form an equational correspondence
as defined by Sabry and Felleisen (1993).
Translating from lambda-mu to dual and then `reloading'
from dual back into lambda-mu yields a term equal to the original term.
Composing the translations with duality on the dual calculus
yields an involutive notion of duality on the lambda-mu-calculus.
A previous notion of duality on the lambda-mu-calculus has
been suggested by Selinger (2001), but it is not involutive.

#### Paper available in:
pdf.

### Call-by-value is dual to call-by-name

Philip Wadler.
International Conference on Functional Programming,
August 2003.
The rules of classical logic may be formulated in pairs corresponding
to De Morgan duals: rules about "and" are dual to rules about "or".
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 in Curien and Herbelin (2000).

#### Talk available in:
pdf.

Philip Wadler,