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

15 hours 28 min ago

15 hours 54 min ago

16 hours 49 min ago

20 hours 30 min ago

1 day 19 hours ago

1 day 19 hours ago

5 days 7 hours ago

5 days 22 hours ago

6 days 39 min ago

1 week 23 hours ago