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.
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.
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).
Philip Wadler,
