×

zbMATH — the first resource for mathematics

Strong normalisation in the \(\pi\)-calculus. (English) Zbl 1101.68705
Summary: We introduce a typed \(\pi\)-calculus where strong normalisation is ensured by typability. Strong normalisation is a useful property in many computational contexts, including distributed systems. In spite of its simplicity, our type discipline captures a wide class of converging name-passing interactive behaviour. The proof of strong normalisability combines methods from typed \(\lambda\)-calculi and linear logic with process-theoretic reasoning. It is adaptable to systems involving state, non-determinism, polymorphism, control and other extensions. Strong normalisation is shown to have significant consequences, including finite axiomatisation of weak bisimilarity, a fully abstract embedding of the simply typed \(\lambda\)-calculus with products and sums and basic liveness in interaction. Strong normalisability has been extensively studied as a fundamental property in functional calculi, term rewriting and logical systems. This work is one of the first steps to extend theories and proof methods for strong normalisability to the context of name-passing processes.

MSC:
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
Software:
Automath; PIPER; PLAN
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Abramsky, S., Computational interpretation of linear logic, Tcs, 111, 3-57, (1993) · Zbl 0791.03003
[2] Abramsky, S., Proofs as processes, Tcs, 135, 5-9, (1994) · Zbl 0850.68297
[3] Abramsky, S.; Jagadeesan, R., Games and full completeness for multiplicative linear logic, Jsl, 59, (1994) · Zbl 0822.03007
[4] Abramsky, S.; Jagadeesan, R.; Malacaria, P., Full abstraction for PCF, Inform. comput., 163, 409-470, (2000) · Zbl 1006.68028
[5] S. Abramsky, Process Realizability, A Tutorial Workshop on Realizability Semantics and Applications, 1999. Available from <web.comlab.ox.ac.uk/oucl/work/samson.abramsky>
[6] T. Altenkirch, P. Dybjer, M. Hofmann, P. Scott, Normalisation by evaluation for typed lambda calculus with coproducts, in: Proceedings of the LICS’01, IEEE, London, 2001, pp. 303-310
[7] Barendregt, H., The lambda calculus: its syntax and semantics, (1984), North-Holland Amsterdam · Zbl 0551.03007
[8] Barendregt, H., Lambda calculi with types, (), 118-120
[9] Bellin, G.; Scott, P.J., On the pi-calculus and linear logic, Tcs, 135, 11-65, (1994) · Zbl 0817.03001
[10] Berger, M.; Honda, K.; Yoshida, N., Sequentiality and the π-calculus, (), 29-45 · Zbl 0981.68037
[11] The full version of 10. Available from <www.dcs.qmw.ac.uk/ kohei>
[12] Berger, M.; Honda, K.; Yoshida, N., Genericity and the π-calculus, (), 103-119 · Zbl 1029.68039
[13] Boreale, M., On expressiveness in internal mobility of name passing calculi, Tcs, 195, 206-226, (1998) · Zbl 0915.68059
[14] Boreale, M.; Sangiorgi, D., Some congruence properties for π-calculus bisimilarities, Tcs, 198, 159-176, (1998) · Zbl 0902.68117
[15] G. Boudol, Asynchrony and the pi-calculus, INRIA Research Report 1702, 1992
[16] G. Boudol, The pi-calculus in direct style, in: Proceedings of the POPL’97, ACM, New York, 1997, pp. 228-241
[17] Boudol, G.; Castellani, I., Noninterference for concurrent programs, (), 382-395 · Zbl 0986.68012
[18] S. Chaki, S. Rajamani, J. Rehof, Types as models: model checking message-passing programs, in: Proceedings of the POPL’02, ACM, New York, 2002 · Zbl 1323.68365
[19] N. Ghani, Adjoint rewriting, Ph.D. Thesis, LFCS, University of Edinburgh, November 1995
[20] Ghani, N., βη-equality from coproducts, (), 171-185 · Zbl 1063.03513
[21] J.H. Gallier, On Girard’s “Candidats de Reductibilité,”, Logic and Computer Science, Academic Press, New York, 1990, pp. 123-203
[22] Gay, S.; Hole, M., Types and subtypes for client – server interactions, (), 74-90
[23] Girard, J.-Y., Linear logic, Tcs, 50, 1-102, (1987) · Zbl 0625.03037
[24] J.-Y. Girard, Y. Lafont, P. Taylor, Proofs and types, vol. 7 of Cambridge Tracts in Theoretical Computer Science, CUP, 1989 · Zbl 0671.68002
[25] Gunter, C.A., Semantics of programming languages: structures and techniques, (1992), MIT Press Cambridge, MA · Zbl 0823.68059
[26] M. Hicks, P. Kakkar, J.T. Moore, C.A. Gunter, S. Nettles, PLAN: a packet language for active networks, in: Proceedings of the International Conference on Functional Programming (ICFP’98), cf. 58 · Zbl 1369.68075
[27] K. Honda, Types for dyadic interaction, in: Proceedings of the CONCUR’93, LNCS, vol. 715, 1993, pp. 509-523 · Zbl 0939.68642
[28] K. Honda, Composing processes, in: Proceedings of the POPL’96, ACM, New York, 1996, pp. 344-357
[29] Honda, K.; Kubo, M.; Vasconcelos, V., Language primitives and type discipline for structured communication-based programming, (), 122-138
[30] Honda, K.; Tokoro, M., An object calculus for asynchronous communication, (), 133-147
[31] K. Honda, V. Vasconcelos, N. Yoshida, Secure information flow as typed process behaviour, in: Proceedings of the ESOP’99, LNCS, vol. 1782, Springer, Berlin, 2000, pp. 180-199. Full version available as MCS Technical Report 01/2000, University of Leicester, 2000 · Zbl 0960.68126
[32] Honda, K.; Yoshida, N., On reduction-based process semantics, (), 437-486 · Zbl 0871.68122
[33] Honda, K.; Yoshida, N., Game-theoretic analysis of call-by-value computation, (), 393-456 · Zbl 0930.68061
[34] K. Honda, N. Yoshida, A uniform type structure for secure information flow, in: Proceedings of the POPL’02, ACM, New York, 2002, pp. 81-92, Full version as a DOC Technical Report, Department of Computing, Imperial College London, 2002/13, August, 2002. Revised in August, 2003. Available from <www.doc.ic.ac.uk/ yoshida> · Zbl 1323.68375
[35] K. Honda, N. Yoshida, Noninterference through Flow Analysis, a DOC Technical Report 2002/14, Imperial College London, revised September 2003, 40 pp. Available from <www.doc.ic.ac.uk/ yoshdia>
[36] Honda, K.; Yoshida, N.; Berger, M., Control in the π-calculus, ()
[37] Huet, G., Confluent reductions: abstract properties and applications to term rewriting systems, J. assoc. comput., 23, 1, 11-21, (1981)
[38] Hyland, M.; Ong, L., On full abstraction for PCF: I, II and III, Inform. comput., 163, 285-408, (2000) · Zbl 1006.68027
[39] A. Igarashi, N. Kobayashi, A generic type system for the pi-calculus, in: Proceedings of the POPL’01, ACM, New York, 2001 · Zbl 1323.68410
[40] Klop, J.W., Term rewriting systems, (), 2-117
[41] Kobayashi, N., A partially deadlock-free typed process calculus, ACM toplas, 20, 2, 436-482, (1998)
[42] Kobayashi, N., Type systems for concurrent processes: from deadlock-freedom to livelock-freedom, time-boundedness, (), 365-389 · Zbl 0998.68085
[43] Kobayashi, N.; Pierce, B.; Turner, D., Linear types and π-calculus, (), 358-371
[44] Laird, J., A deconstruction of non-deterministic classical cut elimination, (), 268-282 · Zbl 0981.03057
[45] O. Laurent, Polarized games, in: Proceedings of the LICS 2002, IEEE, London, 2002, pp. 265-274
[46] O. Laurent, Invited lecture: polarities in linear logic, Linear Logic Workshop, 2002
[47] Lafont, Y., Interaction nets, (), 95-108
[48] Lévy, J.-J., An algebraic interpretation of the λ-β-K-calculus and a labelled λ-calculus, (), 147-165
[49] Merro, M.; Sangiorgi, D., On asynchrony in name-passing calculi, (), 856-867 · Zbl 0910.03019
[50] R. Milner, A Calculus of Communicating Systems, LNCS, vol. 76, Springer, Berlin, 1980 · Zbl 0452.68027
[51] R. Milner, Functions as Processes, MSCS, vol. 2(2), CUP, 1992, pp. 119-146 · Zbl 0773.03012
[52] Milner, R., Polyadic π-calculus: a tutorial, ()
[53] Milner, R.; Parrow, J.G.; Walker, D.J., A calculus of mobile processes, Inform. comput., 100, 1, 1-77, (1992) · Zbl 0752.68037
[54] Mitchell, J., Foundations for programming languages, (1996), MIT Press Cambridge, MA
[55] L. Ong, C. Stewart, A Curry-Howard foundation for functional computation with control, in: Proceedings of the POPL’97, ACM, New York, 1997
[56] Parigot, M., λμ-calculus: an algorithmic interpretation of classical natural deduction, (), 190-201 · Zbl 0925.03092
[57] B.C. Pierce, D. Sangiorgi, Typing and subtyping for mobile processes, in: Proceedings of the LICS’93, IEEE, London, 1993, pp. 187-215 · Zbl 0861.68030
[58] PLAN: A Packet Language for Active Networks, SwitchWare Project, University of Pennsylvania. Available from <http://www.cis.upenn.edu/ switchware/>
[59] Quaglia, P.; Walker, D., On synchronous and asynchronous mobile processes, (), 283-296 · Zbl 0961.68092
[60] D. Sangiorgi, π-Calculus, internal mobility, and agent-passing calculi,TCS 167(2) (1996) 235-271, North-Holland, Amsterdam · Zbl 0874.68103
[61] Sangiorgi, D., The name discipline of uniform receptiveness, (), 303-313 · Zbl 0930.68035
[62] Sangiorgi, D., Types, or: Where’s the difference between CCS and π?, (), 76-97 · Zbl 1012.68137
[63] G. Smith, A new type system for secure information flow, in: Proceedings of the CSFW’01, IEEE, London, 2001
[64] G. Smith, D. Volpano, Secure information flow in a multi-threaded imperative language, in: Proceedings of the POPL’98, ACM, New York, 1998, pp. 355-364
[65] Tait, W., Intensional interpretation of functionals of finite type, I, J. symb. log, 32, 198-212, (1967) · Zbl 0174.01202
[66] Urban, C.; Bierman, G.M., Strong normalisation of cut-elimination in classical logic, Fundam. inform., 45, 1-2, 123-155, (2001) · Zbl 0982.03032
[67] Vasconcelos, V., Typed concurrent objects, (), 100-117
[68] Vasconcelos, V.; Honda, K., Principal typing scheme for polyadic π-calculus, (), 524-538
[69] N. Yoshida, Graph types for monadic mobile processes, in: FST/TCS’16, LNCS vol. 1180, Springer, Berlin, 1996. Full version as LFCS Technical Report, ECS-LFCS-96-350, 1996, pp. 371-387
[70] N. Yoshida, Type-based liveness guarantee in the presence of nontermination and nondeterminism, April 2002. MCS Technical Report, 2002-20, University of Leicester. Available from <www.doc.ic.ac.uk/ yoshida>
[71] N. Yoshida, M. Berger, K. Honda, Strong Normalisation in the π-calculus, in: Proceedings of the LICS’01, IEEE, London, 2001, pp. 311-322. The first full version as MCS Technical Report, 2001-09, University of Leicester, 2001
[72] N. Yoshida, K. Honda, M. Berger, Linearity and bisimulation, in: Proceedings of the Fifth International Conference, Foundations of Software Science and Computer Structures (FoSSaCs 2002), LNCS 2303, pp. 417-433, Springer, Berlin, 2002. A full version as a MCS Technical Report, 2001-48, University of Leicester, 2001. Available from <www.doc.ic.ac.uk/ yoshida> · Zbl 1077.68719
[73] Yoshida, N., Channel dependency types for higher-order mobile processes, Proceedings of the POPL’04, (2004), ACM New York
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.