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. © Springer-Verlag Berlin Heidelberg 2005.
CITATION STYLE
Wadler, P. (2005). Call-by-value is dual to call-by-name - Reloaded. In Lecture Notes in Computer Science (Vol. 3467, pp. 185–203). Springer Verlag. https://doi.org/10.1007/978-3-540-32033-3_15
Mendeley helps you to discover research relevant for your work.