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
25 weeks 4 days ago
25 weeks 4 days ago
25 weeks 4 days ago
47 weeks 5 days ago
52 weeks 18 hours ago
1 year 1 week ago
1 year 1 week ago
1 year 4 weeks ago
1 year 8 weeks ago
1 year 8 weeks ago