We extend a previous type system for the π-calculus that guarantees deadlock-freedom. The previous type systems for deadlockfreedom either lacked a reasonable type inference algorithm or were not strong enough to ensure deadlock-freedom of processes using recursion. Although the extension is fairly simple, the new type system admits type inference and is much more expressive than the previous type systems that admit type inference. In fact, we show that the simply-typed λcalculus with recursion can be encoded into the deadlock-free fragment of our typed π-calculus. To enable analysis of realistic programs, we also present an extension of the type system to handle recursive data structures like lists. Both extensions have already been incorporated into the recent release of TyPiCal, a type-based analyzer for the π-calculus. © Springer-Verlag Berlin Heidelberg 2006.
CITATION STYLE
Kobayashi, N. (2006). A new type system for deadlock-free processes. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4137 LNCS, pp. 233–247). Springer Verlag. https://doi.org/10.1007/11817949_16
Mendeley helps you to discover research relevant for your work.