Call-by-value is Dual to Call-by-name

Research output: Contribution to journalArticlepeer-review

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).
Original languageEnglish
Pages (from-to)189-201
Number of pages13
JournalACM Sigplan Notices
Volume38
Issue number9
DOIs
Publication statusPublished - Aug 2003

Fingerprint

Dive into the research topics of 'Call-by-value is Dual to Call-by-name'. Together they form a unique fingerprint.

Cite this