Abstract
We extend a previous type system for the π-calculus that guarantees deadlock-freedom. The previous type systems for deadlock-freedom 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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Deng, Y., Sangiorgi, D.: Ensuring termination by typability. In: Proceedings of IFIP TCS 2004, pp. 619–632 (2004)
Feret, J.: Abstract interpretation of mobile systems. Journal of Logic and Algebraic Programming 63(1) (2005)
Honda, K., Yoshida, N.: A uniform type structure for secure information flow. In: Proceedings of ACM SIGPLAN/SIGACT Symposium on Principles of Programming Languages, pp. 81–92 (2002)
Kobayashi, N.: TyPiCal: A type-based static analyzer for the pi-calculus, Tool available at: http://www.kb.ecei.tohoku.ac.jp/~koba/typical/
Kobayashi, N.: A partially deadlock-free typed process calculus. ACM Transactions on Programming Languages and Systems 20(2), 436–482 (1998)
Kobayashi, N.: A type system for lock-free processes. Information and Computation 177, 122–159 (2002)
Kobayashi, N.: Type-based information flow analysis for the pi-calculus. Acta Informatica 42(4-5), 291–347 (2005)
Kobayashi, N.: A new type system for deadlock-free processes (2006), Full version available from: http://www.kb.ecei.tohoku.ac.jp/~koba/
Kobayashi, N., Pierce, B.C., Turner, D.N.: Linearity and the pi-calculus. ACM Transactions on Programming Languages and Systems 21(5), 914–947 (1999)
Kobayashi, N., Saito, S., Sumii, E.: An implicitly-typed deadlock-free process calculus. Technical Report TR00-01, Dept. Info. Sci., Univ. of Tokyo (January 2000); A summary has appeared In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, pp. 489–503. Springer, Heidelberg (2000)
Milner, R.: Function as processes. In: Paterson, M. (ed.) ICALP 1990. LNCS, vol. 443, pp. 167–180. Springer, Heidelberg (1990)
Milner, R.: The polyadic π-calculus: a tutorial. In: Bauer, F.L., Brauer, W., Schwichtenberg, H. (eds.) Logic and Algebra of Specification. Springer, Heidelberg (1993)
Pierce, B., Sangiorgi, D.: Typing and subtyping for mobile processes. In: Proceedings of IEEE Symposium on Logic in Computer Science, pp. 376–385 (1993)
Sumii, E., Kobayashi, N.: A generalized deadlock-free process calculus. In: Proc. of Workshop on High-Level Concurrent Language (HLCL 1998). ENTCS, vol. 16(3), pp. 55–77 (1998)
Yoshida, N.: Graph types for monadic mobile processes. In: Chandru, V., Vinay, V. (eds.) FSTTCS 1996. LNCS, vol. 1180, pp. 371–387. Springer, Heidelberg (1996)
Yoshida, N., Berger, M., Honda, K.: Strong normalisation in the pi-calculus. Information and Computation 191(2), 145–202 (2004)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kobayashi, N. (2006). A New Type System for Deadlock-Free Processes. In: Baier, C., Hermanns, H. (eds) CONCUR 2006 – Concurrency Theory. CONCUR 2006. Lecture Notes in Computer Science, vol 4137. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11817949_16
Download citation
DOI: https://doi.org/10.1007/11817949_16
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-37376-6
Online ISBN: 978-3-540-37377-3
eBook Packages: Computer ScienceComputer Science (R0)