Investigations on the dual calculus

Journal article

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.

Authors: Tzevelekos, N

• Publication status: Published
• Peer review status: Peer reviewed
• Publisher: Elsevier
• Journal: Theoretical Computer Science
• Volume: 360
• Issue: 1-3
• Pages: 289–326
• Publication date: 2006-08-01
• Edition: Publisher's version
• DOI: 10.1016/j.tcs.2006.04.009
• ISSN: 0304-3975
• Language: English
• Subjects: Computer science (mathematics)