{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,22]],"date-time":"2026-04-22T07:06:06Z","timestamp":1776841566835,"version":"3.51.2"},"reference-count":35,"publisher":"Springer Science and Business Media LLC","issue":"2-3","license":[{"start":{"date-parts":[[2005,10,11]],"date-time":"2005-10-11T00:00:00Z","timestamp":1128988800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Acta Informatica"],"published-print":{"date-parts":[[2005,11]]},"DOI":"10.1007\/s00236-005-0177-z","type":"journal-article","created":{"date-parts":[[2005,10,11]],"date-time":"2005-10-11T00:39:23Z","timestamp":1128991163000},"page":"191-225","source":"Crossref","is-referenced-by-count":276,"title":["Subtyping for session types in the pi calculus"],"prefix":"10.1007","volume":"42","author":[{"given":"Simon","family":"Gay","sequence":"first","affiliation":[]},{"given":"Malcolm","family":"Hole","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,10,11]]},"reference":[{"issue":"2","key":"177_CR1","doi-asserted-by":"crossref","first-page":"219","DOI":"10.1017\/S095679680400543X","volume":"15","author":"E. Bonelli","year":"2005","unstructured":"Bonelli, E., Compagnoni, A., Gunter, E.: Correspondence assertions for process synchronization in concurrent communication. Journal of Functional Programming 15(2), 219\u2013247 (2005)","journal-title":"Journal of Functional Programming"},{"key":"177_CR2","doi-asserted-by":"crossref","unstructured":"Bonelli, E., Compagnoni, A., Gunter, E.: Typechecking safe process synchronization. In Proceedings of the Third EATCS Workshop on the Foundations of Global Ubiquitous Computing, Electronic Notes on Theoretical Computer Science. Elsevier, 2005. To appear. (2005)","DOI":"10.1016\/j.entcs.2005.05.002"},{"key":"177_CR3","doi-asserted-by":"crossref","unstructured":"Chaki, S., Rajamani, S.K., Rehof, J.: Types as models: model checking message-passing programs. In Proceedings, 29th ACM Symposium on Principles of Programming Languages, pages 45\u201357. ACM Press (2002)","DOI":"10.1145\/503272.503278"},{"key":"177_CR4","doi-asserted-by":"crossref","unstructured":"DeLine, R., F\u00e4hndrich, M.: Enforcing high-level protocols in low-level software. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI) (SIGPLAN Notices 36(5)), pages 59\u201369. ACM Press (2001)","DOI":"10.1145\/378795.378811"},{"key":"177_CR5","doi-asserted-by":"crossref","unstructured":"Dezani-Ciancaglini, M., Yoshida, N., Ahern, A., Drossopolou, S.: A distributed object-oriented language with session types. In Proceedings of the Symposium on Trustworthy Global Computing. Springer, To appear. (2005)","DOI":"10.1007\/11580850_16"},{"key":"177_CR6","doi-asserted-by":"crossref","unstructured":"Gay, S.J.: A sort inference algorithm for the polyadic \u03c0-calculus. In Proceedings, 20th ACM Symposium on Principles of Programming Languages. ACM Press, (1993)","DOI":"10.1145\/158511.158701"},{"key":"177_CR7","doi-asserted-by":"crossref","unstructured":"Gay, S.J., Hole, M.J.: Types and subtypes for client-server interactions. In ESOP'99: Proceedings of the European Symposium on Programming Languages and Systems, volume 1576 of Lecture Notes in Computer Science, pp. 74\u201390. (1999) Springer","DOI":"10.1007\/3-540-49099-X_6"},{"key":"177_CR8","unstructured":"Gay, S.J., Hole, M.J.: Types and subtypes for correct communication in client-server systems. Technical Report TR-2003-131, Department of Computing Science, University of Glasgow (February 2003)"},{"issue":"1","key":"177_CR9","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0304-3975(87)90045-4","volume":"50","author":"J.-Y. Girard","year":"1987","unstructured":"Girard, J.-Y.: Linear Logic. Theoretical Computer Science 50(1), 1\u2013102 (1987)","journal-title":"Theoretical Computer Science"},{"issue":"1\u20133","key":"177_CR10","doi-asserted-by":"crossref","first-page":"379","DOI":"10.1016\/S0304-3975(02)00333-X","volume":"300","author":"A.D. Gordon","year":"2003","unstructured":"Gordon, A.D., Jeffrey, A.: Typing correspondence assertions for communication protocols. Theoretical Computer Science 300(1\u20133), 379\u2013409 (2003)","journal-title":"Theoretical Computer Science"},{"key":"177_CR11","doi-asserted-by":"crossref","unstructured":"Grossman, D.: Type-safe multithreading in cyclone. In Proceedings of the ACM Workshop on Types in Language Design and Implementation (SIGPLAN Notices 38(3)), pp. 13\u201325. ACM Press (2003)","DOI":"10.1145\/604174.604177"},{"key":"177_CR12","doi-asserted-by":"crossref","unstructured":"Grossman, D., Morrisett, G., Jim, T., Hicks, M., Wang, Y., Cheney, J.: Region-based memory management in cyclone. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI) (SIGPLAN Notices 37(5)), pp. 282\u2013293. ACM Press (2002)","DOI":"10.1145\/512529.512563"},{"key":"177_CR13","unstructured":"Hole, M.J., Gay, S.J.: Bounded polymorphism in session types. Technical Report TR-2003-132, Department of Computing Science, University of Glasgow (March 2003)"},{"key":"177_CR14","doi-asserted-by":"crossref","unstructured":"Honda, K.: Types for dyadic interaction. In CONCUR'93: Proceedings of the International Conference on Concurrency Theory, volume 715 of Lecture Notes in Computer Science, pp. 509\u2013523 (Springer, 1993)","DOI":"10.1007\/3-540-57208-2_35"},{"key":"177_CR15","doi-asserted-by":"crossref","unstructured":"Honda, K., Vasconcelos, V., Kubo, M.: Language primitives and type discipline for structured communication-based programming. In ESOP'98: Proceedings of the European Symposium on Programming, volume 1381 of Lecture Notes in Computer Science, pp. 122\u2013138. Springer-Verlag (1998)","DOI":"10.1007\/BFb0053567"},{"issue":"1\u20133","key":"177_CR16","doi-asserted-by":"crossref","first-page":"121","DOI":"10.1016\/S0304-3975(03)00325-6","volume":"311","author":"A. Igarashi","year":"2004","unstructured":"Igarashi, A., Kobayashi, N.: A generic type system for the pi-calculus. Theoretical Computer Science, 311(1\u20133), 121\u2013163 (2004)","journal-title":"Theoretical Computer Science"},{"key":"177_CR17","doi-asserted-by":"crossref","first-page":"436","DOI":"10.1145\/276393.278524","volume":"20","author":"N. Kobayashi","year":"1998","unstructured":"Kobayashi, N.: A partially deadlock-free typed process calculus. ACM Transactions on Programming Languages and Systems 20, 436\u2013482 (1998)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"issue":"5","key":"177_CR18","doi-asserted-by":"crossref","first-page":"914","DOI":"10.1145\/330249.330251","volume":"21","author":"N. Kobayashi","year":"September 1999","unstructured":"Kobayashi, N., Pierce, B.C., Turner, D.N.: Linearity and the Pi-Calculus. ACM Transactions on Programming Languages and Systems 21(5), 914\u2013947 (September 1999)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"issue":"4","key":"177_CR19","first-page":"1","volume":"4","author":"I. Mackie","year":"October 1994","unstructured":"Mackie, I.: Lilac : A functional programming language based on linear logic. Journal of Functional Programming 4(4), 1\u201339 (October 1994)","journal-title":"Journal of Functional Programming"},{"key":"177_CR20","unstructured":"Milner, R.: The polyadic \u03c0-calculus: A tutorial. Technical Report 91-180, Laboratory for Foundations of Computer Science, Department of Computer Science, University of Edinburgh (1991)"},{"issue":"1","key":"177_CR21","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0890-5401(92)90008-4","volume":"100","author":"R. Milner","year":"September 1992","unstructured":"Milner, R., Parrow, J., Walker, D.: A calculus of mobile processes, I and II. Information and Computation 100(1), 1\u201377 (September 1992)","journal-title":"Information and Computation"},{"key":"177_CR22","doi-asserted-by":"crossref","unstructured":"Myers, J., Rose, M.: Post office protocol version 3. Internet Standards RFC1939. (May 1996)","DOI":"10.17487\/rfc1939"},{"key":"177_CR23","doi-asserted-by":"crossref","unstructured":"Neubauer, M., Thiemann, P.: An implementation of session types. In Practical Aspects of Declarative Languages (PADL'04), volume 3057 of Lecture Notes in Computer Science, pp. 56\u201370 (Springer, 2004)","DOI":"10.1007\/978-3-540-24836-1_5"},{"key":"177_CR24","doi-asserted-by":"crossref","unstructured":"Neubauer, M., Thiemann, P.: Protocol specialization. In Proceedings of the Second Asian Symposium on Programming Languages and Systems (APLAS 2004), volume 3302 of Lecture Notes in Computer Science, pp. 246\u2013261 (Springer, 2004)","DOI":"10.1007\/978-3-540-30477-7_17"},{"key":"177_CR25","unstructured":"Pierce, B.C.: Types and programming languages. MIT Press (2002)"},{"key":"177_CR26","doi-asserted-by":"crossref","unstructured":"Pierce, B.C., Sangiorgi, D.: Typing and subtyping for mobile processes. Mathematical Structures in Computer Science, 6(5) (1996)","DOI":"10.1017\/S096012950007002X"},{"key":"177_CR27","doi-asserted-by":"crossref","unstructured":"Pierce, B.C., Sangiorgi, D.: Behavioral equivalence in the polymorphic pi-calculus. Journal of the ACM 47(3), (2000)","DOI":"10.1145\/337244.337261"},{"key":"177_CR28","doi-asserted-by":"crossref","unstructured":"Pierce, B.C., Turner, D.N.: Pict: A programming language based on the pi-calculus. In G. Plotkin, C. Stirling, and M. Tofte, editors, Proof, Language and Interaction: Essays in Honour of Robin Milner. MIT Press (2000)","DOI":"10.7551\/mitpress\/5641.003.0022"},{"key":"177_CR29","first-page":"8th","volume":"Analysis","author":"Rajamani","year":"2001","unstructured":"Rajamani, S.K., Rehof, J.: A behavioral module system for the pi-calculus. In Static Analysis: 8th International Symposium, SAS 2001, volume 2126 of Lecture Notes in Computer Science, pp. 375\u2013394. Springer (2001)","journal-title":"In Static"},{"key":"177_CR30","unstructured":"Sangiorgi, D., Walker, D.: The \u03c0-calculus: a Theory of Mobile Processes. Cambridge University Press (2001)"},{"key":"177_CR31","doi-asserted-by":"crossref","unstructured":"Takeuchi, K., Honda, K., Kubo, M.: An interaction-based language and its typing system. In PARLE '94: Parallel Architectures and Languages Europe, volume 817 of Lecture Notes in Computer Science, Springer (1994)","DOI":"10.1007\/3-540-58184-7_118"},{"key":"177_CR32","unstructured":"Turner, D.N.: The Polymorphic Pi-Calculus: theory and implementation. PhD thesis, University of Edinburgh (1996)"},{"key":"177_CR33","doi-asserted-by":"crossref","unstructured":"Vallecillo, A., Vasconcelos, V.T., Ravara, A.: Typing the behavior of objects and components using session types. In International Workshop on Foundations of Coordination Languages and Software Architectures, volume 68(3) of Electronic Notes in Theoretical Computer Science. Elsevier (2003)","DOI":"10.1016\/S1571-0661(05)80382-2"},{"key":"177_CR34","doi-asserted-by":"crossref","unstructured":"Vasconcelos, V.T., Honda, K.: Principal typing schemes in a polyadic \u03c0-calculus. In CONCUR'93: Proceedings of the International Conference on Concurrency Theory, volume 715 of Lecture Notes in Computer Science. Springer, (1993)","DOI":"10.1007\/3-540-57208-2_36"},{"key":"177_CR35","doi-asserted-by":"crossref","unstructured":"Vasconcelos, V.T., Ravara, A., Gay, S.J.: Session types for functional multithreading. In CONCUR'04: Proceedings of the International Conference on Concurrency Theory, volume 3170 of Lecture Notes in Computer Science, pages 497\u2013511. Springer. Full version to appear in Theoretical Computer Science. (2004)","DOI":"10.1007\/978-3-540-28644-8_32"}],"container-title":["Acta Informatica"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-005-0177-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00236-005-0177-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-005-0177-z","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,4]],"date-time":"2025-01-04T21:51:52Z","timestamp":1736027512000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s00236-005-0177-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005,10,11]]},"references-count":35,"journal-issue":{"issue":"2-3","published-print":{"date-parts":[[2005,11]]}},"alternative-id":["177"],"URL":"https:\/\/doi.org\/10.1007\/s00236-005-0177-z","relation":{},"ISSN":["0001-5903","1432-0525"],"issn-type":[{"value":"0001-5903","type":"print"},{"value":"1432-0525","type":"electronic"}],"subject":[],"published":{"date-parts":[[2005,10,11]]}}}