Call-by-Value Is Dual to Call-by-Name - Reloaded

10 years 9 months ago
Call-by-Value Is Dual to Call-by-Name - Reloaded
We consider the relation of the dual calculus of Wadler (2003) to the λµ-calculus of Parigot (1992). We give translations from the λµ-calculus into the dual calculus and back again. The translations form an equational correspondence as defined by Sabry and Felleisen (1993). In particular, translating from λµ to dual and then ‘reloading’ from dual back into λµ yields a term equal to the original term. Composing the translations with duality on the dual calculus yields an involutive notion of duality on the λµ-calculus. A previous notion of duality on the λµcalculus has been suggested by Selinger (2001), but it is not involutive. Note This paper uses color to clarify the relation of types and terms, and of source and target calculi. If the URL below is not in blue please download the color version from or google ‘wadler dual reloaded’.
Philip Wadler
Added 28 Jun 2010
Updated 28 Jun 2010
Type Conference
Year 2005
Where RTA
Authors Philip Wadler
Comments (0)