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 20 hours ago
3 days 15 hours ago
2 weeks 16 hours ago
2 weeks 6 days ago
3 weeks 6 days ago
5 weeks 4 days ago
6 weeks 20 hours ago
7 weeks 1 day ago
7 weeks 5 days ago
7 weeks 5 days ago