Skip to main content

Investigations on the Dual Calculus

Nikos Tzevelekos

Abstract

The Dual Calculus, proposed by Wadler in 2003, is the outcome of two distinct lines of research in theoretical computer science: A. Efforts to extend the Curry-Howard isomorphism, established between 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 project is aiming at introducing the Dual Calculus, examining its syntactic behaviour, and investigating possible extensions of it to polymorphic types.

Institution
Oxford University Computing Laboratory
Month
November
Number
RR−04−21
Year
2004