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

1 day 16 hours ago

1 day 22 hours ago

2 days 9 hours ago

2 days 9 hours ago

5 days 17 hours ago

5 days 19 hours ago

5 days 23 hours ago

6 days 16 hours ago

1 week 2 hours ago

1 week 1 day ago