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

19 hours 26 min ago

19 hours 30 min ago

1 day 13 min ago

1 day 1 hour ago

1 day 5 hours ago

1 day 10 hours ago

1 day 10 hours ago

1 day 22 hours ago

1 day 23 hours ago

2 days 6 hours ago