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 weeks 6 days ago
24 weeks 1 day ago
25 weeks 5 days ago
25 weeks 5 days ago
28 weeks 3 days ago
33 weeks 17 hours ago
33 weeks 18 hours ago
33 weeks 3 days ago
33 weeks 3 days ago
36 weeks 2 days ago