Call-by-Value Is Dual to Call-by-Name – Reloaded TeX Export

@incollection{citeulike:6064470, abstract = {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 \$\$ \texttt{http://homepages.inf.ed.ac.uk/wadler/} \$\$ or google 'wadler dual reloaded'.}, author = {Wadler, Philip}, citeulike-article-id = {6064470}, citeulike-linkout-0 = {http://www.springerlink.com/content/h68j46gtdcuvwmuk}, journal = {Term Rewriting and Applications}, keywords = {call-by-name, call-by-value, dual\_calculus}, pages = {185--203}, posted-at = {2009-11-03 20:26:38}, priority = {3}, title = {Call-by-Value Is Dual to Call-by-Name – Reloaded}, url = {http://www.springerlink.com/content/h68j46gtdcuvwmuk}, year = {2005} }

TY - CHAP ID - citeulike:6064470 L3 - citeulike-article-id:6064470 N2 - 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 $$ \texttt{http://homepages.inf.ed.ac.uk/wadler/} $$ or google ‘wadler dual reloaded’. JF - Term Rewriting and Applications EP - 203 TI - Call-by-Value Is Dual to Call-by-Name – Reloaded SP - 185 KW - call-by-name KW - call-by-value KW - dual_calculus AU - Wadler, Philip PY - 2005/// UR - http://www.springerlink.com/content/h68j46gtdcuvwmuk ER -