The pi-Calculus in Direct Style

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.

a.k.a. Blue Calculus

## Recent comments

14 hours 24 min ago

16 hours 37 min ago

18 hours 6 min ago

19 hours 54 min ago

21 hours 13 min ago

1 day 3 hours ago

1 day 18 hours ago

1 day 19 hours ago

1 day 19 hours ago

1 day 19 hours ago