[Prev][Next][Index][Thread]
A Partially Deadlock-free Process Calculus
[------ The Types Forum ------- http://www.dcs.gla.ac.uk/~types ------]
We would like to announce that the following technical report is
available from:
ftp://ftp.is.s.u-tokyo.ac.jp/pub/tech-reports/TR96-02-{a4,letter}.ps.Z
Any comments are welcome.
--------
A Partially Deadlock-free Typed Process Calculus (I)
-- A Simple System --
Naoki Kobayashi
Univeristy of Tokyo
Abstract:
Concurrency primitives play an important role in
describing programs on parallel/distributed environments
and also in writing interactive programs. Theoretical
supports of 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,
capturing the order of channel uses.
With the type system, for example, the 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.
------
Naoki Kobayashi
Department of Information Science
Faculty of Science
University of Tokyo
7-3-1 Hongo, Bunkyo-ku,
Tokyo 113, Japan
e-mail:koba@is.s.u-tokyo.ac.jp