Technical Report (TR97-02) Cover Page

Title:

A Partially Deadlock-free Typed Process Calculus (II)

Authors:

Naoki Kobayashi

Key words and phrases:

deadlock, process calculus, type system, linear type

Abstract:

We propose a novel static type system for a process calculus, which ensures both partial deadlock-freedom and partial confluence. The key novel ideas are (1) introduction of the order of channel use as type information, and (2) classification of communication channels into reliable and unreliable channels based on their usage and a guarantee of the usage by the type system. We can ensure that communication on reliable channels never causes deadlock and also that certain reliable channels never introduce nondeterminism. With the type system, for example, call-by-value and and call-by-name simply typed lambda-calculi can be encoded into the deadlock-free and confluent fragment of our process calculus; we can therefore recover the behavior of typed lambda-calculi at the level of process calculi. We also show that typical concurrent objects and call-by-need simply typed lambda-calculus can also be encoded into the deadlock-free fragment.

Report date:

February, 1997

Written language:

English

Total number of pages:

40

Number of references:

26

Any other identifying information of this report:

A revised version of this paper is available here . A summary is presented at IEEE Symposium on Logic in Computer Science (LICS'97).

Distribution statement:

First issue 35 copies.

Supplementary notes: