{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T09:04:43Z","timestamp":1770282283130,"version":"3.49.0"},"reference-count":33,"publisher":"Cambridge University Press (CUP)","issue":"5","license":[{"start":{"date-parts":[[2018,4,19]],"date-time":"2018-04-19T00:00:00Z","timestamp":1524096000000},"content-version":"unspecified","delay-in-days":7870,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[1996,10]]},"abstract":"<jats:p>The <jats:italic>\u03c0<\/jats:italic>-calculus is a process algebra that supports mobility by focusing on the communication of channels. Milner's presentation of the <jats:italic>\u03c0<\/jats:italic>-calculus includes a type system assigning arities to channels and enforcing a corresponding discipline in their use. We extend Milner's language of types by distinguishing between the ability to read from a channel, the ability to write to a channel, and the ability both to read and to write. This refinement gives rise to a natural subtype relation similar to those studied in typed <jats:italic>\u03bb<\/jats:italic>-calculi. The greater precision of our type discipline yields stronger versions of standard theorems on the <jats:italic>\u03c0<\/jats:italic>-calculus. These can be used, for example, to obtain the validity of <jats:italic>\u03b2<\/jats:italic>-reduction for the more efficient of Milner's encodings of the call-by-value <jats:italic>\u03bb<\/jats:italic>-calculus, which fails in the ordinary <jats:italic>\u03c0<\/jats:italic>-calculus. We define the syntax, typing, subtyping, and operational semantics of our calculus, prove that the typing rules are sound, apply the system to Milner's <jats:italic>\u03bb<\/jats:italic>-calculus encodings, and sketch extensions to higher-order process calculi and polymorphic typing.<\/jats:p>","DOI":"10.1017\/s096012950007002x","type":"journal-article","created":{"date-parts":[[2019,5,12]],"date-time":"2019-05-12T20:14:05Z","timestamp":1557692045000},"page":"409-453","source":"Crossref","is-referenced-by-count":172,"title":["Typing and subtyping for mobile processes"],"prefix":"10.1017","volume":"6","author":[{"given":"Benjamin","family":"Pierce","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Davide","family":"Sangiorgi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2018,4,19]]},"reference":[{"key":"S096012950007002X_ref017","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(78)90014-4"},{"key":"S096012950007002X_ref021","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0026570"},{"key":"S096012950007002X_ref019","doi-asserted-by":"crossref","unstructured":"Odersky M. (1995) Polarized Name Passing. In: Proceedings of Foundations of Software Technology and Theoretical Computer Science. Springer-Verlag Lecture Notes in Computer Science.","DOI":"10.1007\/3-540-60692-0_58"},{"key":"S096012950007002X_ref018","doi-asserted-by":"publisher","DOI":"10.1145\/174675.174538"},{"key":"S096012950007002X_ref013","doi-asserted-by":"crossref","unstructured":"Milner R. (1990) Functions as Processes. Research Report 1154, INRIA, Sophia Antipolis. (Final version in Journal of Mathem. Structures in Computer Science (1992) 2 (2) 119-141.)","DOI":"10.1017\/S0960129500001407"},{"key":"S096012950007002X_ref024","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(75)90017-1"},{"key":"S096012950007002X_ref012","volume-title":"Communication and Concurrency","author":"Milner","year":"1989"},{"key":"S096012950007002X_ref011","doi-asserted-by":"crossref","unstructured":"Kobayashi N. , Pierce B. C. and Turner D. N. (1996) Linearity and the Pi-Calculus. Principles of Programming Languages.","DOI":"10.1145\/237721.237804"},{"key":"S096012950007002X_ref022","unstructured":"Pierce B. C. and Turner D. N. (1995b) Pict: A Programming Language Based on the Pi-Calculus (to appear)."},{"key":"S096012950007002X_ref009","unstructured":"Girard J.-Y. (1972) Interpretation fonctionelle et elimination des coupures de l'arithmetique d'ordre sup\u00e9rieur, Ph.D. thesis, Universit\u00e9 Paris VII."},{"key":"S096012950007002X_ref004","doi-asserted-by":"publisher","DOI":"10.1145\/6041.6042"},{"key":"S096012950007002X_ref025","first-page":"408","volume-title":"Proc. Colloque sur la Programmation","volume":"19","author":"Reynolds","year":"1974"},{"key":"S096012950007002X_ref007","doi-asserted-by":"crossref","DOI":"10.7146\/dpb.v15i208.7559","volume-title":"A Calculus of Communicating Systems with Label-Passing","author":"Engberg","year":"1986"},{"key":"S096012950007002X_ref015","first-page":"685","volume-title":"Proceedings 19th ICALP","volume":"623","author":"Milner","year":"1992"},{"key":"S096012950007002X_ref028","unstructured":"Sangiorgi D. (1992) Expressing Mobility in Process Algebras: First-Order and Higher-Order Paradigms, Ph.D. thesis CST-99-93, Department of Computer Science, University of Edinburgh."},{"key":"S096012950007002X_ref020","unstructured":"Parrow J. and Sangiorgi D. (1993) Algebraic Theories for Name-Passing Calculi. Tech. rept. ECS-LFCS-93-262, LFCS, Dept. of Comp. Sci., Edinburgh Univ. (To appear in Information and Compuation. Short version in Proc. REX Summer School\/Symposium 1993, Springer-Verlag Lecture Notes in Computer Science 803.)"},{"key":"S096012950007002X_ref002","doi-asserted-by":"publisher","DOI":"10.1145\/155183.155231"},{"key":"S096012950007002X_ref033","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1995.1018"},{"key":"S096012950007002X_ref016","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(92)90008-4"},{"key":"S096012950007002X_ref005","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(83)90059-2"},{"key":"S096012950007002X_ref001","first-page":"65","volume-title":"Research Topics in Functional Programming","author":"Abramsky","year":"1989"},{"key":"S096012950007002X_ref006","doi-asserted-by":"publisher","DOI":"10.1016\/1385-7258(72)90034-0"},{"key":"S096012950007002X_ref014","volume-title":"Logic and Algebra of Specification","author":"Milner","year":"1991"},{"key":"S096012950007002X_ref010","first-page":"186","volume-title":"Computer Science Logic, Selected Papers from CSL'92","volume":"702","author":"Glavan","year":"1993"},{"key":"S096012950007002X_ref029","doi-asserted-by":"crossref","unstructured":"Sangiorgi D. (1993) A Theory of Bisimulation for the \u03c0-calculus. Tech. rept. ECS\u2013LFCS\u201393\u2013270. LFCS, Dept. of Comp. Sci., Edinburgh Univ. (Extended Abstract in Proc. CONCUR \u201993, Springer-Verlag Lecture Notes in Computer Science 715.)","DOI":"10.1007\/3-540-57208-2_10"},{"key":"S096012950007002X_ref023","volume-title":"Workshop on Type Theory and its Application to Computer Systems","author":"Pierce","year":"1993"},{"key":"S096012950007002X_ref003","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-17184-3_38"},{"key":"S096012950007002X_ref008","doi-asserted-by":"crossref","unstructured":"Gay S. J. (1993) A Sort Inference Algorithm for the Polyadic \u03c0-Calculus. In: Proceedings of the Twentieth ACM Symposium on Principles of Programming Languages.","DOI":"10.1145\/158511.158701"},{"key":"S096012950007002X_ref026","first-page":"185","volume-title":"Mathematical Foundations of Software Development","author":"Reynolds","year":"1985"},{"key":"S096012950007002X_ref030","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-58184-7_118"},{"key":"S096012950007002X_ref031","unstructured":"Turner D. N. (1996). The Polymorphic Pi-calculus: Theory and Implementation, Ph.D. thesis, LFCS, University of Edinburgh."},{"key":"S096012950007002X_ref032","unstructured":"Vasconcelos V. T. and Honda K. (1993) Principal Typing Schemes in a Polyadic Pi-Calculus. In: Proceedings of CONCUR \u201993. Also available as Keio University Report CS-92-004."},{"key":"S096012950007002X_ref027","volume-title":"Preliminary Design of the Programming Language Forsythe","author":"Reynolds","year":"1988"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S096012950007002X","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,12]],"date-time":"2019-05-12T20:14:23Z","timestamp":1557692063000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S096012950007002X\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996,10]]},"references-count":33,"journal-issue":{"issue":"5","published-print":{"date-parts":[[1996,10]]}},"alternative-id":["S096012950007002X"],"URL":"https:\/\/doi.org\/10.1017\/s096012950007002x","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[1996,10]]}}}