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.
Details
| Institution |
Oxford University Computing Laboratory |
| Month |
November |
| Number |
RR−04−21 |
| Year |
2004 |