[Prev][Next][Index][Thread]

Paper announcement: types and concurrency



This is to announce the availability of the paper

   "Typing the use of resources in a concurrent calculus",

to be published in the Proceedings of ASIAN'97, the Asian Computing
Science Conference, Kathmandu, Nepal, December 9-11, 1997 (LNCS to
appear), at the URL

   http://www.inria.fr/meije/personnel/Gerard.Boudol.html

Here is the 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.