Hostname: page-component-76fb5796d-dfsvx Total loading time: 0 Render date: 2024-04-25T11:39:41.579Z Has data issue: false hasContentIssue false

From λ to π; or, Rediscovering continuations

Published online by Cambridge University Press:  01 August 1999

DAVIDE SANGIORGI
Affiliation:
INRIA-Sophia Antipolis, 2004 Rue des Lucioles, B.P. 93, 06902 Sophia Antipolis, France. Email: davide.sangiorgi@inria.fr.

Abstract

We study the relationship between the encodings of the λ-calculus into π-calculus, the Continuation Passing Style (CPS) transforms, and the compilation of the Higher-Order π-calculus (HOπ) into π-calculus. We factorise the π-calculus encodings of (untyped as well as simply-typed) call-by-name and call-by-value λ-calculus into three steps: a CPS transform, the inclusion of CPS terms into HOπ and the compilation from HOπ to π-calculus. The factorisations are used both to derive the encodings and to prove their correctness.

Type
Research Article
Copyright
© 1999 Cambridge University Press

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)