Informatics Report Series


Report   

EDI-INF-RR-0587


Related Pages

Report (by Number) Index
Report (by Date) Index
Author Index
Institute Index

Home
Title:Call-by-value is dual to call-by-name
Authors: Philip Wadler
Date:Sep 2003
Publication Title:ACM International Conference on Functional Programming (ICFP)
Publisher:ACM
Publication Type:Conference Paper Publication Status:Published
Page Nos:189-201
DOI:10.1145/944705.944723 ISBN/ISSN:1-58113-75
Abstract:
The rules of classical logic may be formulated in pairs corresponding to De Morgan duals: rules about & are dual to rules about V. A line of work, including that of Filinski (1989), Griffin (1990), Parigot (1992), Danos, Joinet, and Schellinx (1995), Selinger (1998,2001), and Curien and Herbelin (2000), has led to the startling conclusion that call-by-value is the de Morgan dual of call-by-name.This paper presents a dual calculus that corresponds to the classical sequent calculus of Gentzen (1935) in the same way that the lambda calculus of Church (1932,1940) corresponds to the intuitionistic natural deduction of Gentzen (1935). The paper includes crisp formulations of call-by-value and call-by-name that are obviously dual; no similar formulations appear in the literature. The paper gives a CPS translation and its inverse, and shows that the translation is both sound and complete, strengthening a result in Curien and Herbelin (2000).
Links To Paper
ACM Digital Portal
Bibtex format
@InProceedings{EDI-INF-RR-0587,
author = { Philip Wadler },
title = {Call-by-value is dual to call-by-name},
book title = {ACM International Conference on Functional Programming (ICFP)},
publisher = {ACM},
year = 2003,
month = {Sep},
pages = {189-201},
doi = {10.1145/944705.944723},
url = {http://portal.acm.org/citation.cfm?id=944723},
}


Home : Publications : Report 

Please mail <reports@inf.ed.ac.uk> with any changes or corrections.
Unless explicitly stated otherwise, all material is copyright The University of Edinburgh