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 7 hours ago
1 day 7 hours ago
2 days 17 hours ago
3 days 9 min ago
3 days 10 hours ago
3 days 20 hours ago
4 days 19 min ago
4 days 5 hours ago
4 days 5 hours ago
4 days 14 hours ago