[Prev][Next][Index][Thread]
Paper announcement: Implicitly-Typed Deadlock-Free Process Calculus
We would like to announce the availability of the technical report
below, which is available at
http://www.yl.is.s.u-tokyo.ac.jp/~koba/pub/deadlock-inference.ps.gz.
Any comments are welcome.
Naoki Kobayashi
University of Tokyo
-------
An Implicitly-Typed Deadlock-Free Process Calculus
Naoki Kobayashi, Shin Saito, and Eijiro Sumii
ABSTRACT:
We extend Kobayashi and Sumii's type system for the deadlock-free
Pi-calculus and develop a type reconstruction algorithm. Kobayashi
and Sumii's type system is a generalization of Kobayashi, Pierce, and
Turner's linear pi-calculus, and it helps high-level reasoning about
concurrent programs by guaranteeing that communication on certain
channels will eventually succeed. It can ensure, for example, that a
process implementing a function really behaves like a function.
However, because it lacked a type reconstruction algorithm and
required rather complicated type annotations, it was impractical to
apply it to real concurrent languages. We have therefore developed a
type reconstruction algorithm for an extension of the type system. The
key novelties that made it possible are generalization of the channel usage
calculus (which was first introduced in Sumii and Kobayashi's previous type
system) and a subusage relation.