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 (CBV) reduction in lambda calculus is dual to call-by-name (CBN) 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’ CBV reduction relation. Finally, extensions of the calculus to second-order types are briefly introduced.

Keywords: Dual Calculus; Classical lambda calculi; Curry–Howard isomorphism; Continuations