Abstract
We present a type discipline for the π-calculus which precisely captures the notion of sequential functional computation as a specific class of name passing interactive behaviour. The typed calculus allows direct interpretation of both call-by-name and call-by-value sequential functions. The precision of the representation is demonstrated by way of a fully abstract encoding of PCF. The result shows how a typed π-calculus can be used as a descriptive tool for a significant class of programming languages without losing the latter’s semantic properties. Close correspondence with games semantics and process-theoretic reasoning techniques are together used to establish full abstraction.
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
Abramsky, S., Computational interpretation of linear logic. TCS, Vol. 111, 1993.
Abramsky, S., Honda, K. and McCusker, G., A Fully Abstract Game Semantics for General References. LICS, 334–344, IEEE, 1998.
Abramsky, S., Jagadeesan, R. and Malacaria, P., Full Abstraction for PCF. Info. & Comp., Vol. 163, 2000.
Berger, M. Honda, K. and N. Yoshida. Sequentiality and the π-Calculus. To appear as a QMW DCS Technical Report, 2001.
Berger, M. Honda, K. and N. Yoshida. Genericity in the π-Calculus. To appear as a QMW DCS Technical Report, 2001.
Berry, G. and Curien, P. L., Sequential algorithms on concrete data structures TCS, 20(3), 265–321, North-Holland, 1982.
Boreale, M. and Sangiorgi, D., Some congruence properties for π-calculus bisimilarities, TCS, 198, 159–176, 1998.
Boudol, G., Asynchrony and the pi-calculus, INRIA Research Report 1702, 1992.
Boudol, G., The pi-calculus in direct style, POPL’97, 228–241, ACM, 1997.
Curien, P. L., Sequentiality and full abstraction. Proc. of Application of Categories in Computer Science, LNM 177, 86–94, Cambridge Press, 1995.
Fiore, M. and Honda, K., Recursive Types in Games: axiomatics and process representation, LICS’98, 345–356, IEEE, 1998.
Gay, S. and Hole, M., Types and Subtypes for Client-Server Interactions, ESOP’99, LNCS 1576, 74–90, Springer, 1999.
Girard, J.-Y., Linear Logic, TCS, Vol. 50, 1–102, 1987.
Gunter, C., Semantics of Programming Languages: Structures and Techniques, MIT Press, 1992.
Honda, K., Types for Dyadic Interaction. CONCUR’93, LNCS 715, 509–523, 1993.
Honda, K., Composing Processes, POPL’96, 344–357, ACM, 1996.
Honda, K., Kubo, M. and Vasconcelos, V., Language Primitives and Type Discipline for Structured Communication-Based Programming. ESOP’98, LNCS 1381, 122–138. Springer-Verlag, 1998.
Honda, K. and Tokoro, M., An Object Calculus for Asynchronous Communication. ECOOP’91, LNCS 512, 133–147, Springer-Verlag 1991.
Honda, K. Vasconcelos, V., and Yoshida, N. Secure Information Flow as Typed Process Behaviour, ESOP’ 99, LNCS 1782, 180–199, Springer-Verlag, 2000.
Honda, K. and Yoshida, N. Game-theoretic analysis of call-by-value computation. TCS Vol. 221 (1999), 393–456, North-Holland, 1999.
Kobayashi, N., A partially deadlock-free typed process calculus, ACM TOPLAS, Vol. 20,No. 2, 436–482, 1998.
Kobayashi, N., Pierce, B., and Turner, D., Linear Types and π-calculus, POPL’96, 358–371, ACM Press, 1996.
Hyland, M. and Ong, L., On Full Abstraction for PCF: I, II and III. 130 pages, 1994. To appear in Info. & Comp.
Hyland, M. and Ong, L., Pi-calculus, dialogue games and PCF, FPCA’95, ACM, 1995.
Laird, J., Full abstraction for functional languages with control, LICS’97, IEEE, 1997.
McCusker, G., Games and Full Abstraction for FPC. LICS’96, IEEE, 1996.
Milner, R., Fully abstract models of typed lambda calculi. TCS, 4:1–22, 1977.
Milner, R., Functions as Processes. MSCS, 2(2), 119–146, CUP, 1992.
Milner, R., Polyadic π-Calculus: a tutorial. Proceedings of the International Summer School on Logic Algebra of Specification, Marktoberdorf, 1992.
Pierce, B.C. and Sangiorgi. D, Typing and subtyping for mobile processes. LICS’93, 187–215, IEEE, 1993.
Quaglia, P. and Walker, D., On Synchronous and Asynchronous Mobile Processes, FoSSaCS 00, LNCS 1784, 283–296, Springer, 2000.
Sangiorgi, D., Expressing Mobility in Process Algebras: First Order and Higher Order Paradigms. Ph.D. Thesis, University of Edinburgh, 1992.
Sangiorgi, D. π-calculus, internal mobility, and agent-passing calculi. TCS, 167(2):235–271, North-Holland, 1996.
Sangiorgi, D., The name discipline of uniform receptiveness, ICALP’97, LNCS 1256, 303–313, Springer, 1997.
Vasconcelos, V., Typed concurrent objects. ECOOP’94, LNCS 821, 100–117. Springer, 1994.
Vasconcelos, V. and Honda, K., Principal Typing Scheme for Polyadic π-Calculus. CONCUR’93, LNCS 715, 524–538, Springer-Verlag, 1993.
Yoshida, N., Graph Types for Monadic Mobile Processes, FST/TCS’16, LNCS 1180, 371–387, Springer-Verlag, December, 1996.
Yoshida, N., Berger, M. and Honda, K., Strong Normalisation in the π-Calculus, To appear as a MCS Technical Report, University of Leicester, 2001.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Berger, M., Honda, K., Yoshida, N. (2001). Sequentiality and the π-Calculus. In: Abramsky, S. (eds) Typed Lambda Calculi and Applications. TLCA 2001. Lecture Notes in Computer Science, vol 2044. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45413-6_7
Download citation
DOI: https://doi.org/10.1007/3-540-45413-6_7
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-41960-0
Online ISBN: 978-3-540-45413-7
eBook Packages: Springer Book Archive