The rules of classical logic may be formulated in pairs corresponding to DeMorgan duals: rules about And are dual to rules about Or. The traditional Curry-Howard correspondence relates the lambda calculus of Church (1932,1940) to the intuitionistic natural deduction of Gentzen (1935). Extensions of Curry-Howard relate \lambda calculi with operations like call/cc to classical logics. This line of results includes the work of Filinski (1989), Griffin (1990), Parigot (1992), Barbanera and Berardi (1996), Selinger (1998,2001), and Curien and Herbelin (2000). A startling conclusion of this line of work, not widely appreciated, is that call-by-value is the de Morgan dual of call-by-name.
This paper presents a dual calculus, which 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 unifies and sharpens previous results regarding the translation from a dual calculus into continuation-passing style. Curien and Herbelin (2000) give a soundness result for beta reductions, but do not show completeness and do not treat eta reductions. Selinger (2001) gives a soundness and completeness result and treats beta and eta equivalences, but considers only equations and not reductions. This paper gives a soundness and completeness result for beta and eta reductions.