Atsushi Igarashi
ABSTRACT
We propose a general, powerful framework of type systems for the π-calculus, and show that we can obtain as its instances a variety of type systems guaranteeing non-trivial properties like deadlock-freedom and race-freedom. A key idea is to express types and type environments as abstract processes: We can check various properties of a process by checking the corresponding properties of its type environment. The framework clarifies the essence of recent complex type systems, and it also enables sharing of a large amount of work such as a proof of type preservation, making it easy to develop new type systems.
- 1.L. Cardelli and A. D. Gordon. Anytime, anywhere: Modal logics for mobile ambients. In Proceedings of A CM SIGPLAN/SIGA CT Symposium on Principles of Programming Languages, pages 365-377, 2000.]] Google Scholar
Digital Library
- 2.P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proceedings of ACM SIGPLAN/SIGACT Symposium on Principles of Programming Languages, pages 238-252, 1977.]] Google ScholarDigital Library
- 3.M. F/ihndrich and A. Aiken. Program analysis using mixed term and set constraints. In Proceedings of SAS'97, LNCS 1302, pages 114-126. Springer-Verlag, 1997.]] Google ScholarDigital Library
- 4.C. Flanagan and M. Abadi. Object types against races. In CONCUR'99, LNCS 1664, pages 288-303. Springer- Verlag, 1999.]] Google ScholarDigital Library
- 5.C. Flanagan and M. Abadi. Types for safe locking. In Proceedings of ESOP 1999, LNCS 1576, pages 91-108, 1999.]] Google ScholarDigital Library
- 6.C. Flanagan and S. N. Freund. Type-based race detection for Java. In Proceedings of ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 219-232, 2000.]] Google ScholarDigital Library
- 7.S. J. Gay. A sort inference algorithm for the polyadiccalculus. In Proceedings of A CM SIGPLAN/SIGA CT Symposium on Principles of Programming Languages, pages 429-438, 1993.]] Google ScholarDigital Library
- 8.M. Hennessy and J. Riely. Information flow vs. resource access in the information asynchronous pi-calculus. In Proceedings of ICALP 2000, LNCS 1853. Springer- Verlag, 2000.]] Google ScholarDigital Library
- 9.K. Honda. Composing processes. In Proceedings of ACM SIGPLAN/SIGACT Symposium on Principles of Programming Languages, pages 344-357, 1996.]] Google ScholarDigital Library
- 10.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. Springer-Verlag, 2000.]] Google ScholarDigital Library
- 11.A. Igarashi and N. Kobayashi. A generic type system for the pi-calculus. Tech. rep., Department of Information Science, University of Tokyo, 2000. to appear.]]Google Scholar
- 12.A. Igarashi and N. Kobayashi. Type reconstruction for linear pi-calculus with I/O subtyping. Information and Computation, 161:1-44, 2000.]] Google ScholarDigital Library
- 13.C. B. Jones. A pi-calculus semantics for an objectbased design notation. In Proceedings of CONCUR '93, LNCS, pages 158-172. Springer-Verlag, 1993.]] Google ScholarDigital Library
- 14.N. Kobayashi. A partially deadlock-free typed process calculus. ACM Transactions on Programming Languages and Systems, 20(2):436-482, 1998.]] Google ScholarDigital Library
- 15.N. Kobayashi. Quasi-linear types. In Proceedings of ACM SIGPLAN/SIGACT Symposium on Principles of Programming Languages, pages 29-42, 1999.]] Google ScholarDigital Library
- 16.N. Kobayashi. Type systems for concurrent processes: From deadlock-freedom to livelock-freedom, time-boundedness. In Proceedings of IFIP International Conference on Theoretical Computer Science (TCS2000), LNCS 1872, pages 365-389, 2000.]] Google ScholarDigital Library
- 17.N. Kobayashi, B. C. Pierce, and D. N. Turner. Linearity and the pi-cMculus. A CM Transactions on Programming Languages and Systems, 21(5):914-947, 1999.]] Google ScholarDigital Library
- 18.N. Kobayashi, E. Sumii, and S. Saito. An implicitlytyped deadlock-free process calculus. In Proceedings of CONCUR2000, LNCS 1877, pages 489-503. Springer- Verlag, 2000.]] Google ScholarDigital Library
- 19.N. Kobayashi and A. Yonezawa. Towards foundations for concurrent object-oriented programming - types and language design. Theory and Practice of Object Systems, 1(4):243-268, 1995.]] Google ScholarDigital Library
- 20.B. K~nig. Generating type systems for process graphs. In Proceedings of CONCUR '99, LNCS 1664, pages 352- 367. Springer-Verlag, 1999.]] Google ScholarDigital Library
- 21.B. K~nig. Analysing input/output-capabilities of mobile processes with a generic type system. In Proceedings of ICALP 2000, LNCS 1853. Springer-Verlag, 2000.]] Google ScholarDigital Library
- 22.R. Milner. Communication and Concurrency. Prentice Hall, 1989.]] Google ScholarDigital Library
- 23.R. Milner. The polyadic v-calculus: a tutorial. In F. L. Bauer, W. Brauer, and H. Schwichtenberg, editors, Logic and Algebra of Specification. Springer-Verlag, 1993.]]Google ScholarCross Ref
- 24.R. Milner. Calculi for interaction. Acta Informatica, 33(8):707-737, 1996.]]Google ScholarDigital Library
- 25.H. R. Nielson and F. Nielson. Higher-order concurrent programs with finite communication topology. In Proceedings of ACM SIGPLAN/SIGACT Symposium on Principles of Programming Languages, pages 84-97, 1994.]] Google ScholarDigital Library
- 26.F. Pessaux and X. Leroy. Type-based analysis of uncaught exceptions. In Proceedings of ACM SIG- PLAN/SIGACT Symposium on Principles of Programming Languages, pages 276-290, 1999.]] Google ScholarDigital Library
- 27.B. Pierce and D. Sangiorgi. Typing and subtyping for mobile processes. Mathematical Structures in Computer Science, 6(5):409-454, 1996.]]Google ScholarCross Ref
- 28.B. Pierce and D. Sangiorgi. Behavioral equivalence in the polymorphic pi-calculus. Journal of the Association for Computing Machinery (JACM), 47(5):531-584, 2000.]] Google ScholarDigital Library
- 29.B. C. Pierce and D. N. Turner. Concurrent objects in a process calculus. In Theory and Practice of Parallel Programming (TPPP), Sendal, Japan (Nov. 199), LNCS 907, pages 187-215. Springer-Verlag, 1995.]] Google Scholar
- 30.F. Puntigam and C. Peter. Changeable interfaces and promised messages for concurrent components. In Proceedings of the 1999 A CM Symposium on Applied Computing, pages 141-145, 1999.]] Google ScholarDigital Library
- 31.A. Ravara and V. Vasconcelos. Typing non-uniform concurrent objects. In Proceedings of CONCUR2000, LNCS 1877, pages 474-488, 2000.]] Google ScholarDigital Library
- 32.C. Stifling. Modal and temporal logics for processes. In Logics for Concurrency, LNCS 1043, pages 149-237, 1996.]] Google ScholarDigital Library
- 33.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.]]Google ScholarCross Ref
- 34.J.-P. Talpin and P. Jouvelot. Polymorphic type, region and effect inference. Journal of Functional Programming, 2(3):245-271, 1992.]]Google ScholarCross Ref
- 35.J.-P. Talpin and P. Jouvelot. The type and effect discipline. In Proceedings of IEEE Symposium on Logic in Computer Science, pages 162-173, 1992.]]Google ScholarCross Ref
- 36.M. Tofte and J.-P. Talpin. Implementation of the callby-value lambda-calculus using a stack of regions. In Proceedings of ACM SIGPLAN/SIGACT Symposium on Principles off Programming Languages, pages 188- 201, 1994.]] Google ScholarDigital Library
- 37.V. T. Vaseoncelos and K. Honda. Principal typing schemes in a polyadic 7-calculus. In CONCUR'93, LNCS 715, pages 524-538. Springer-Verlag, 1993.]] Google ScholarDigital Library
- 38.N. Yoshida. Graph types for monadic mobile processes. In FST/TCS'16, LNCS 1180, pages 371-387. Springer- Verlag, 1996.]] Google Scholar
Index Terms
- A generic type system for the Pi-calculus
Recommendations
A generic type system for the Pi-calculus
We propose a general, powerful framework of type systems for the π-calculus, and show that we can obtain as its instances a variety of type systems guaranteeing non-trivial properties like deadlock-freedom and race-freedom. A key idea is to express ...
A generic type system for the Pi-calculus
We propose a general, powerful framework of type systems for the π-calculus, and show that we can obtain as its instances a variety of type systems guaranteeing non-trivial properties like deadlock-freedom and race-freedom. A key idea is to express ...
Type inference for a distributed π-calculus
Special issue on 12th European symposium on programming (ESOP 2003)We study the type inference problem for a distributed π-calculus with explicit notions of locality and migration. Location types involve names that may be bound in terms. This requires an accurate new approach. We define a notion of principal typing. We ...
Comments