Investigations on the Dual Calculus

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.