Technical Report (TR96-02) Cover Page

Title:

A Partially Deadlock-free Typed Process Calculus (I) -- A Simple System --

Authors:

Naoki Kobayashi

Key words and phrases:

deadlock, process calculus, type system, linear type, linear channel

Abstract:

Concurrency primitives play an important role in describing programs on parallel/distributed environments and also in writing interactive programs. Theoretical supports for concurrency primitives, however, have so far been very limited. Several type systems have been recently proposed through process calculi, but most of them do not solve inherent problems in concurrent programs: deadlock and non-determinism. We propose a novel type system that ensures both partial deadlock-freedom and partial confluence, along the line of Kobayashi, Pierce, and Turner's linear channel type system. The technical novelty lies in the use of a poset as a type environment, by which capturing the order of channel uses. With the type system, for example, call-by-value simply typed \(\lambda\)-calculus can be encoded into the deadlock-free and confluent fragment of our process calculus, thus, we can recover behavior of the typed \(\lambda\)-calculus at the level of process calculi.

Report date:

September 4, 1996

Written language:

English

Total number of pages:

32

Number of references:

26

Any other identifying information of this report:

Distribution statement:

First issue 35 copies.

Supplementary notes: