Typing the use of resources in a concurrent calculus , ASIAN'97, the Asian Computing Science Conference, Kathmandu, Nepal, LNCS 1345 (1997) 239-253.

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]