Abstract
A type system for the polyadic π-calculus is introduced. Within this system every process possesses a type. A class of consistent types is isolated which is such that if a process can be assigned a consistent type then it is free from type errors under reduction. Further, for each type which is not consistent there is a process with that type which is not free from type errors. It is decidable whether or not a given process can be assigned a consistent type. Algorithms for type checking and type inference are given.
Supported by a grant from the U.K. Engineering and Physical Sciences Research Council
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
S. Gay. A sort inference algorithm for the polyadic π-calculus. In Proceedings of 20th POPL. ACM Press, 1993.
C. Jones. A pi-calculus semantics for an object-based design notation. In Proceedings of CONCUR'93, pages 158–172. Springer, 1993.
X. Liu and D. Walker. Confluence of processes and systems of objects. In Proceedings of CAAP'95. Springer, to appear.
R. Milner. Action structures. Technical report, University of Edinburgh, 1992.
R. Milner. Functions as processes. Mathematical Structures in Computer Science, 2:119–141, 1992.
R. Milner. The polyadic π-calculus: a tutorial. In Logic and Algebra of Specification. Springer, 1992.
R. Milner, J. Parrow, and D. Walker. A calculus of mobile processes, parts 1 and 2. Information and Computation, 100:1–77, 1992.
B. Pierce. Programming in the π-calculus. Technical report, University of Edinburgh, 1994.
B. Pierce and D. Sangiorgi. Typing and subtyping for mobile processes. In Proceedings of LICS'93, pages 376–385. Computer Society Press, 1993.
D. Sangiorgi. Expressing mobility in process algebras: first-order and higher-order paradigms. PhD thesis, University of Edinburgh, 1992.
D. Sangiorgi. The lazy lambda-calculus in a concurrency scenario. Information and Computation, 111:120–153, 1994.
D. Sangiorgi. Locality and true-concurrency in calculi for mobile processes. In Proceedings of TACS'94, pages 405–420. Springer, 1994.
D. Turner. PhD thesis, University of Edinburgh, forthcoming.
V. Vasconcelos and K. Honda. Principal typing schemes in the polyadic π-calculus. In Proceedings of CONCUR'93. Springer, 1993.
D. Walker. Objects in the π-calculus. Information and Computation, 116:253–271, 1995.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1995 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Liu, X., Walker, D. (1995). A polymorphic type system for the polyadic π-calculus. In: Lee, I., Smolka, S.A. (eds) CONCUR '95: Concurrency Theory. CONCUR 1995. Lecture Notes in Computer Science, vol 962. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-60218-6_8
Download citation
DOI: https://doi.org/10.1007/3-540-60218-6_8
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-60218-7
Online ISBN: 978-3-540-44738-2
eBook Packages: Springer Book Archive