## The pi-Calculus in Direct Style

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

## Comment viewing options

### And even more "direct"

The Deep Blue Calculus
We develop a calculus which is a "direct" descendant of the blue calculus of Boudol [Bou97]. This calculus is both an extension of Abadi & Cardelli's &-calculus [AC96] and the Milner's pi-calculus [Mil93]. We give a simple type system that is a direct extension of any type fragment considered in [AC96] encodable into the pi-calculus. The type system enjoys Subject Reduction. We provide finally an adequate CPS transform from our calculus to the blue calculus. This transform shows that the latter can be seen as a "target language", while our calculus provide a very expressive and promising notation for higher-order object-oriented concurrent programming languages.

Should I start googling for even deeper blues??!

### Review

Just several points that I brought home:
1. Application of call-by-name lambda is broken down to two constructs (def and application) of name-passing lambda - so can be used as a syntactic sugar thereafter (page 1)
2. def is broken down to three constructs (restriction, parallel, and decl) of blue calculus - so can be used as a syntactic sugar thereafter (page 2)
3. the resulted calculus directly subsumes both CBN lambda and pi (that was actually a disappointment to understand that CBV does not play so nice - but I might got it wrong - still have to grok CPS section which I skipped on the first reading)
4. declared references are suggested to be separated from abstracted variables (pages 11-12)
While not unifying CBV and CBN directly, this calculus seems as a good start point for a small (or big) concurrent PL.

Also, it was a pleasure to see how presenting complex constructs in terms of simpler ("big" application via "small" application and def, then def via nu, par, and decl) allowed a more flexible and expressive structure where it's needed, while preserving simplicity where it was enough.

I will be glad to hear objections (especially from Derek, as he probably was right about CPS after all).