Higher-Order and Symbolic Computation, 11(2)177-208
The pi-Calculus in Direct StyleGérard Boudol, INRIA Sophia-Antipolis, BP 93, Sophia Antipolis Cedex, France
|
Abstract: We introduce a calculus which is a direct extension
of both the lambda and the pi calculi. We give a simple type system
for it, that encompasses both Curry's type inference for the
lambda-calculus, and Milner's sorting for the pi-calculus as
particular cases of typing. We observe that the various continuation
passing style transformations for lambda-terms, written in our
calculus, actually correspond to encodings already given by Milner and
others for evaluation strategies of lambda-terms into the
pi-calculus. Furthermore, the associated sortings correspond to
well-known double negation translations on types. Finally we provide
an adequate CPS transform from our calculus to the pi-calculus. This
shows that the latter may be regarded as an "assembly language", while
our calculus seems to provide a better programming notation for
higher-order concurrency. We conclude by discussing some alternative
design decisions.
Keywords: lambda-calculus, pi-calculus, types, continuation passing style, |
This article can be downloaded [here].
![[picture of journal cover]](../LISP.JPG)