Abstract
We extend Kobayashi and Sumii’s type system for the deadlock-free π-calculus and develop a type reconstruction algorithm. Kobayashi and Sumii’s type system 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, applying it to real concurrent languages was impractical. 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 usages (which specifies how each communication channel is used) and a subusage relation.
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.
Similar content being viewed by others
References
G. Boudol. Typing the use of resources in a concurrent calculus. In Proceedings of ASIAN’97, LNCS 1345, pages 239–253, 1997.
K. Honda, V. Vasconcelos, and N. Yoshida. Secure information flow as typed process behaviour. In Proc. of European Symposium on Programming (ESOP) 2000, LNCS 1782, pp. 180–199, 2000.
J. Esparza and M. Nielsen. Decidability issues for Petri nets-a survey. Journal of Information Processing and Cybernetics, 30(3):143–160, 1994.
A. Igarashi and N. Kobayashi. Type reconstruction for linear pi-calculus with I/O subtyping. Information and Computation. To appear. A preliminary summary appeared in Proceedings of SAS’97, LNCS 1302, pp.187–201.
N. Kobayashi. A partially deadlock-free typed process calculus. ACM Transactions on Programming Languages and Systems, 20(2):436–482, 1998.
N. Kobayashi, B. C. Pierce, and D. N. Turner. Linearity and the pi-calculus. ACM Transactions on Programming Languages and Systems, 21(5):914–947, 1999. A preliminary summary appeared in Proceedings of POPL’96, pp.358–371.
N. Kobayashi, S. Saito, and E. Sumii. An implicitly-typed deadlock-free process calculus. Technical Report TR00-01, Dept. Info. Sci., Univ. of Tokyo, January 2000. Available at http://www.yl.is.s.u-tokyo.ac.jp/~koba/publications.html.
R. Milner. The polyadic π-calculus: a tutorial. In Logic and Algebra of Specification. Springer-Verlag, 1993.
R. Milner, J. Parrow, and D. Walker. A calculus of mobile processes, I, II. Information and Computation, 100:1–77, September 1992.
O. Nierstrasz. Regular types for active objects. In Object-Oriented Software Composition, chapter 4, pages 99–121. Prentice Hall, 1995. A preliminary version appeared in Proceedings of OOPSLA’93, pp.1–15.
B. Pierce and D. Sangiorgi. Typing and subtyping for mobile processes. Mathematical Structures in Computer Science, 6(5):409–454, 1996.
B. C. Pierce and D. N. Turner. Pict: A programming language based on the pi-calculus. To appear in Proof, Language, and Interaction: Essays in Honour of Robin Milner, MIT Press, 2000
F. Puntigam. Coordination requirements expressed in types for active objects. In Proceedings of ECOOP’97, LNCS 1241, pages 367–388, 1997.
J. H. Reppy. CML: A higher-order concurrent language. In Proceedings of PLDI’91, pages 293–305, 1991.
D. Sangiorgi. The name discipline of uniform receptiveness. Theoretical Computer Science, 221(1–2), pages 457–493, 1999.
E. Sumii and N. Kobayashi. A generalized deadlock-free process calculus. In Proc. of Workshop on High-Level Concurrent Language (HLCL’98), ENTCS 16(3), pages 55–77, 1998.
K. Takeuchi, K. Honda, and M. Kubo. An interaction-based language and its typing system. In Proceedings of PARLE’94, LNCS 817, pages 398–413, 1994.
N. Yoshida. Graph types for monadic mobile processes. In FST/TCS’16, LNCS 1180, pages 371–387, 1996.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kobayashi, N., Saito, S., Sumii, E. (2000). An Implicitly-Typed Deadlock-Free Process Calculus. In: Palamidessi, C. (eds) CONCUR 2000 — Concurrency Theory. CONCUR 2000. Lecture Notes in Computer Science, vol 1877. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44618-4_35
Download citation
DOI: https://doi.org/10.1007/3-540-44618-4_35
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67897-7
Online ISBN: 978-3-540-44618-7
eBook Packages: Springer Book Archive