Abstract:
We introduce a new type system for the blue calculus -- a variant of the pi-calculus that directly contains the lambda-calculus. Our notion of type is built upon a combination of Curry-Church simple types and Hennessy-Milner logic with recursion. We interpret a modality as the type of a process offering a resource of some type on a given name. In the typing system this is used in a kind of logical cut rule, ensuring that a message to the name will meet a corresponding offer. We show that our calculus is type safe, that is, types are preserved along the computations.

[PostScript, .ps.gz]