Abstract:
This work is concerned with the foundations of higher-order concurrent programming. We focus on languages based on Milner's pi-calculus. Motivated by the observation that an indirect style of programming, where one explicitly manages ``result channels'', is enforced in such languages, we aim at designing a similar, but more flexible model for higher-order concurrency.

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.

[Preliminary version PostScript, .ps.gz ]