zbMATH — the first resource for mathematics

The \(\pi\)-calculus in direct style. (English) Zbl 0934.68037
Summary: 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.

68N18 Functional programming and lambda calculus
Full Text: DOI