# 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.

##### MSC:
 68N18 Functional programming and lambda calculus
##### Keywords:
$$\pi$$ calculi; $$\lambda$$-calculus
Full Text: