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

6 days 5 hours ago

1 week 1 day ago

1 week 1 day ago

1 week 1 day ago

1 week 1 day ago

1 week 1 day ago

1 week 1 day ago

1 week 1 day ago

1 week 1 day ago

1 week 1 day ago