Abstract
We formulate a typed formalism for concurrency where types denote freely composable structure of dyadic interaction in the symmetric scheme. The resulting calculus is a typed reconstruction of name passing process calculi. Systems with both the explicit and implicit typing disciplines, where types form a simple hierarchy of types, are presented, which are proved to be in accordance with each other. A typed variant of bisimilarity is formulated and it is shown that typed β-equality has a clean embedding in the bisimilarity. Name reference structure induced by the simple hierarchy of types is studied, which fully characterises the typable terms in the set of untyped terms. It turns out that the name reference structure results in the deadlock-free property for a subset of terms with a certain regular structure, showing behavioural significance of the simple type discipline.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Abramsky, S., Computational interpretations of linear logic. Technical Report DOC 90/20, Imperial College, Department of Computing, October 1990. to appear in Theoretical Computer Science.
Barendregt, H. and Hemerik, K., Types in lambda calculi and programming languages. In Proceeding of ESOP 90, 1990.
Boudol, G., Asynchrony and π-calculus. Manuscript. 1992.
Engberg, U. and Nielsen, M., A Calculus of Communicating Systems with Label Passing. Research Report DAIMI PB-208, Computer Science Department, University of Aarhus, 1986.
Gay, S. J., A sort inference algorizm for the poliadic π-calculus. POPL, 1993.
Hindley R., The Principal Type-Scheme in Objects in Combinatory Logic, Trans. American. Math. Soc. 146.
Honda, K. and Tokoro, M., An Object Calculus for Asynchronous Communication, In: Proc. of European Conference on Object-Oriented Programming, LNCS, Springer-Verlag, July 1991.
Honda, K., Representing Functions in an Object Calculus, a typescript, 19pp, October 1991. Revised version as Keio CS Report 92-005, 1992.
Honda, K., Two Bisimilarities in ν-calculus, September 1992, submitted. Revised version as Keio CS Report 92-002, 1992.
Honda, K., Types for Dyadic Interaction (the full version), Keio CS Report 92-003, 1993.
Honda, K., and Yoshida, N., On Process Based Reduction Semantics, Keio CS technical report 93-002, 1993.
Lafont, Y., Interaction Nets, POPL 1990.
Milner, R., A Theory of Type Polymorphism in Programming, Journal of ACM, 1978.
Milner, R., Parrow, J.G. and Walker, D.J., A Calculus of Mobile Processes. Part I, II. ECS-LFCS-89-85/86, Edinburgh University, 1989.
Milner, R., Functions as Processes. In Automate, Language and Programming, LNCS 443, 1990.
Milner,R. and Sangiriorgi, D., Barbed Bisimulation, ICALP, 1992.
Milner, R., Polyadic π-calculus, LFCS report, Edinburgh University 1992.
Mitchell, J., Type Systems for Programming Languages, Handbook of Theoretical Computer Science, P 367–458, Elsevier Science Publishers B.V., 1990.
Pierce, B. and Sangiorgi, D., Typing and Subtyping for Mobile Processes.
Vasco, V. and Honda, K., Principal typing scheme for polyadic π-Calculus, in this volume.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1993 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Honda, K. (1993). Types for dyadic interaction. In: Best, E. (eds) CONCUR'93. CONCUR 1993. Lecture Notes in Computer Science, vol 715. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-57208-2_35
Download citation
DOI: https://doi.org/10.1007/3-540-57208-2_35
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-57208-4
Online ISBN: 978-3-540-47968-0
eBook Packages: Springer Book Archive