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

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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 http://homepages.inf.ed.ac.uk/wadler/ http://homepages.inf.ed.ac.uk/wadler/ or google ‘wadler dual reloaded’.
Original languageEnglish
Title of host publicationTerm Rewriting and Applications
Subtitle of host publication16th International Conference, RTA 2005, Nara, Japan, April 19-21, 2005, Proceedings
PublisherSpringer Berlin Heidelberg
Pages185-203
Number of pages19
ISBN (Electronic)978-3-540-32033-3
ISBN (Print)978-3-540-25596-3
DOIs
Publication statusPublished - 2005

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin Heidelberg
Volume3467
ISSN (Print)0302-9743

Fingerprint

Dive into the research topics of 'Call-by-Value Is Dual to Call-by-Name - Reloaded'. Together they form a unique fingerprint.

Cite this