Investigations on the dual calculus

The Dual Calculus, proposed recently by Wadler, is the outcome of two distinct lines of research in theoretical computer science: A. Efforts to extend the Curry-Howard isomorphism, established between the simply-typed lambda calculus and intuitionistic logic, to classical logic. B. Efforts to establish the tacit conjecture that call-by-value reduction in lambda calculus is dual to call-by-name reduction. This paper initially investigates relations of the Dual Calculus to other calculi, namely the simply-typed lambda calculus and the Symmetric lambda calculus. Moreover, Church-Rosser and Strong Normalization properties are proven for the calculus ’ call-by-value reduction relation. Finally, extensions of the calculus to second-order types are briefly introduced.