{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T02:13:49Z","timestamp":1775873629088,"version":"3.50.1"},"reference-count":181,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2016,4,5]],"date-time":"2016-04-05T00:00:00Z","timestamp":1459814400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100000921","name":"European Cooperation in Science and Technology","doi-asserted-by":"publisher","award":["IC1201 BETTY"],"award-info":[{"award-number":["IC1201 BETTY"]}],"id":[{"id":"10.13039\/501100000921","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100005856","name":"Faculdade de Ci\u00eancias e Tecnologia, Universidade Nova de Lisboa","doi-asserted-by":"publisher","award":["UID\/CEC\/00408\/2013"],"award-info":[{"award-number":["UID\/CEC\/00408\/2013"]}],"id":[{"id":"10.13039\/501100005856","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Comput. Surv."],"published-print":{"date-parts":[[2017,3,31]]},"abstract":"<jats:p>Behavioural type systems, usually associated to concurrent or distributed computations, encompass concepts such as interfaces, communication protocols, and contracts, in addition to the traditional input\/output operations. The behavioural type of a software component specifies its expected patterns of interaction using expressive type languages, so types can be used to determine automatically whether the component interacts correctly with other components. Two related important notions of behavioural types are those of session types and behavioural contracts. This article surveys the main accomplishments of the last 20 years within these two approaches.<\/jats:p>","DOI":"10.1145\/2873052","type":"journal-article","created":{"date-parts":[[2016,4,5]],"date-time":"2016-04-05T15:18:51Z","timestamp":1459869531000},"page":"1-36","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":133,"title":["Foundations of Session Types and Behavioural Contracts"],"prefix":"10.1145","volume":"49","author":[{"given":"Hans","family":"H\u00fcttel","sequence":"first","affiliation":[{"name":"Aalborg University, Aalborg \u00d8, Denmark"}]},{"given":"Ivan","family":"Lanese","sequence":"additional","affiliation":[{"name":"University of Bologna\/INRIA, Bologna, Italy"}]},{"given":"Vasco T.","family":"Vasconcelos","sequence":"additional","affiliation":[{"name":"University of Lisbon, Lisbon, Portugal"}]},{"given":"Lu\u00eds","family":"Caires","sequence":"additional","affiliation":[{"name":"Universidade Nova de Lisboa, Caparica, Portugal"}]},{"given":"Marco","family":"Carbone","sequence":"additional","affiliation":[{"name":"ITU Copenhagen"}]},{"given":"Pierre-Malo","family":"Deni\u00e9lou","sequence":"additional","affiliation":[{"name":"Royal Holloway, University of London, Egham Hill, United Kingdom"}]},{"given":"Dimitris","family":"Mostrous","sequence":"additional","affiliation":[{"name":"University of Lisbon, Lisbon, Portugal"}]},{"given":"Luca","family":"Padovani","sequence":"additional","affiliation":[{"name":"University of Turin, Torino, Italy"}]},{"given":"Ant\u00f3nio","family":"Ravara","sequence":"additional","affiliation":[{"name":"Universidade Nova de Lisboa, Caparica, Portugal"}]},{"given":"Emilio","family":"Tuosto","sequence":"additional","affiliation":[{"name":"University of Leicester, Leicester, United Kingdom"}]},{"given":"Hugo Torres","family":"Vieira","sequence":"additional","affiliation":[{"name":"IMT School for Advanced Studies Lucca, Lucca, Italy"}]},{"given":"Gianluigi","family":"Zavattaro","sequence":"additional","affiliation":[{"name":"University of Bologna\/INRIA, Bologna, Italy"}]}],"member":"320","published-online":{"date-parts":[[2016,4,5]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"A Theory of Objects","author":"Abadi Mart\u00edn","unstructured":"Mart\u00edn Abadi and Luca Cardelli . 1996. A Theory of Objects . Springer , Berlin . Mart\u00edn Abadi and Luca Cardelli. 1996. A Theory of Objects. Springer, Berlin."},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2008.08.017"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2009.10.011"},{"key":"e_1_2_1_4_1","volume-title":"FOSSACS (LNCS)","author":"Acciai Lucia","unstructured":"Lucia Acciai , Michele Boreale , and Gianluigi Zavattaro . 2010. On the relationship between spatial logics and behavioral simulations . In FOSSACS (LNCS) , Vol. 6014 . Springer , Berlin , 146--160. Lucia Acciai, Michele Boreale, and Gianluigi Zavattaro. 2010. On the relationship between spatial logics and behavioral simulations. In FOSSACS (LNCS), Vol. 6014. Springer, Berlin, 146--160."},{"key":"e_1_2_1_5_1","volume-title":"Vasco Thudichum Vasconcelos, and Hugo Torres Vieira","author":"Baltazar Pedro","year":"2012","unstructured":"Pedro Baltazar , Lu\u00eds Caires , Vasco Thudichum Vasconcelos, and Hugo Torres Vieira . 2012 a. A type system for flexible role assignment in multiparty communicating systems. In TGC (LNCS), Vol. 8191 . Springer , Berlin, 82--96. Pedro Baltazar, Lu\u00eds Caires, Vasco Thudichum Vasconcelos, and Hugo Torres Vieira. 2012a. A type system for flexible role assignment in multiparty communicating systems. In TGC (LNCS), Vol. 8191. Springer, Berlin, 82--96."},{"key":"e_1_2_1_6_1","volume-title":"LINEARITY (EPTCS)","author":"Baltazar Pedro","unstructured":"Pedro Baltazar , Dimitris Mostrous , and Vasco Thudichum Vasconcelos . 2012b. Linearly refined session types . In LINEARITY (EPTCS) , Vol. 101 . Open Publishing Association , Sydney , 38--49. Pedro Baltazar, Dimitris Mostrous, and Vasco Thudichum Vasconcelos. 2012b. Linearly refined session types. In LINEARITY (EPTCS), Vol. 101. Open Publishing Association, Sydney, 38--49."},{"key":"e_1_2_1_7_1","volume-title":"PPDP","author":"Barbanera Franco","unstructured":"Franco Barbanera and Ugo de\u2019 Liguoro . 2010. Two notions of sub-behaviour for session-based client\/server systems . In PPDP . ACM , New York, NY , 155--164. Franco Barbanera and Ugo de\u2019Liguoro. 2010. Two notions of sub-behaviour for session-based client\/server systems. In PPDP. ACM, New York, NY, 155--164."},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1995.1086"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.2307\/2273659"},{"key":"e_1_2_1_10_1","volume-title":"Lambda Calculus With Types","author":"Barendregt Henk","unstructured":"Henk Barendregt , Wil Dekkers , and Richard Statman . 2013. Lambda Calculus With Types . Cambridge University Press , Cambridge . Henk Barendregt, Wil Dekkers, and Richard Statman. 2013. Lambda Calculus With Types. Cambridge University Press, Cambridge."},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2007.70740"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2014.11.015"},{"key":"e_1_2_1_13_1","volume-title":"FMOODS\/FORTE (LNCS)","author":"Bartoletti Massimo","unstructured":"Massimo Bartoletti , Alceste Scalas , Emilio Tuosto , and Roberto Zunino . 2013. Honesty by typing . In FMOODS\/FORTE (LNCS) , Vol. 7892 . Springer , Berlin , 305--320. Massimo Bartoletti, Alceste Scalas, Emilio Tuosto, and Roberto Zunino. 2013. Honesty by typing. In FMOODS\/FORTE (LNCS), Vol. 7892. Springer, Berlin, 305--320."},{"key":"e_1_2_1_14_1","first-page":"5","article-title":"Contract-oriented computing in CO2. Sci","volume":"22","author":"Bartoletti Massimo","year":"2012","unstructured":"Massimo Bartoletti , Emilio Tuosto , and Roberto Zunino . 2012 a. Contract-oriented computing in CO2. Sci . Ann. Comp. Sci. 22 , 1 (2012), 5 -- 60 . Massimo Bartoletti, Emilio Tuosto, and Roberto Zunino. 2012a. Contract-oriented computing in CO2. Sci. Ann. Comp. Sci. 22, 1 (2012), 5--60.","journal-title":"Ann. Comp. Sci."},{"key":"e_1_2_1_15_1","volume-title":"COORDINATION (LNCS)","author":"Bartoletti Massimo","unstructured":"Massimo Bartoletti , Emilio Tuosto , and Roberto Zunino . 2012b. On the realizability of contracts in dishonest systems . In COORDINATION (LNCS) , Vol. 7274 . Springer , Berlin , 245--260. Massimo Bartoletti, Emilio Tuosto, and Roberto Zunino. 2012b. On the realizability of contracts in dishonest systems. In COORDINATION (LNCS), Vol. 7274. Springer, Berlin, 245--260."},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-005-0175-1"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2245276.2232097"},{"key":"e_1_2_1_19_1","volume-title":"SEFM Workshops (LNCS)","volume":"8368","author":"Bernardi Giovanni","year":"2013","unstructured":"Giovanni Bernardi and Matthew Hennessy . 2013 . Compliance and testing preorders differ . In SEFM Workshops (LNCS) , Vol. 8368 . Springer, Berlin, 69--81. Giovanni Bernardi and Matthew Hennessy. 2013. Compliance and testing preorders differ. In SEFM Workshops (LNCS), Vol. 8368. Springer, Berlin, 69--81."},{"key":"e_1_2_1_20_1","volume-title":"CONCUR (LNCS)","author":"Bernardi Giovanni","unstructured":"Giovanni Bernardi and Matthew Hennessy . 2014. Using higher-order contracts to model session types (extended abstract) . In CONCUR (LNCS) , Vol. 8704 . Springer , Berlin , 387--401. Giovanni Bernardi and Matthew Hennessy. 2014. Using higher-order contracts to model session types (extended abstract). In CONCUR (LNCS), Vol. 8704. Springer, Berlin, 387--401."},{"key":"e_1_2_1_21_1","volume-title":"Concurrency, Graphs and Models (LNCS)","author":"Bettini Lorenzo","unstructured":"Lorenzo Bettini , Sara Capecchi , Mariangiola Dezani-Ciancaglini , Elena Giachino , and Betti Venneri . 2008. Session and union types for object oriented programming . In Concurrency, Graphs and Models (LNCS) , Vol. 5065 . Springer , Berlin , 659--680. Lorenzo Bettini, Sara Capecchi, Mariangiola Dezani-Ciancaglini, Elena Giachino, and Betti Venneri. 2008. Session and union types for object oriented programming. In Concurrency, Graphs and Models (LNCS), Vol. 5065. Springer, Berlin, 659--680."},{"key":"e_1_2_1_22_1","volume-title":"CONCUR (LNCS)","author":"Bocchi Laura","unstructured":"Laura Bocchi , Kohei Honda , Emilio Tuosto , and Nobuko Yoshida . 2010. A theory of design-by-contract for distributed multiparty interactions . In CONCUR (LNCS) , Vol. 6269 . Springer , Berlin , 162--176. Laura Bocchi, Kohei Honda, Emilio Tuosto, and Nobuko Yoshida. 2010. A theory of design-by-contract for distributed multiparty interactions. In CONCUR (LNCS), Vol. 6269. Springer, Berlin, 162--176."},{"key":"e_1_2_1_23_1","first-page":"61","article-title":"Three algorithms and a methodology for amending contracts for choreographies. Sci","volume":"22","author":"Bocchi Laura","year":"2012","unstructured":"Laura Bocchi , Julien Lange , and Emilio Tuosto . 2012 . Three algorithms and a methodology for amending contracts for choreographies. Sci . Ann. Comp. Sci. 22 , 1 (2012), 61 -- 104 . Laura Bocchi, Julien Lange, and Emilio Tuosto. 2012. Three algorithms and a methodology for amending contracts for choreographies. Sci. Ann. Comp. Sci. 22, 1 (2012), 61--104.","journal-title":"Ann. Comp. Sci."},{"key":"e_1_2_1_24_1","volume-title":"Gunter","author":"Bonelli Eduardo","year":"2005","unstructured":"Eduardo Bonelli , Adriana B. Compagnoni , and Elsa L . Gunter . 2005 . Typechecking safe process synchronization. In FGUC (ENTCS), Vol. 138 . Elsevier , Amsterdam, 3--22. Eduardo Bonelli, Adriana B. Compagnoni, and Elsa L. Gunter. 2005. Typechecking safe process synchronization. In FGUC (ENTCS), Vol. 138. Elsevier, Amsterdam, 3--22."},{"key":"e_1_2_1_25_1","volume-title":"Ivan Lanese, Michele Loreti, Francisco Martins, Ugo Montanari, Ant\u00f3nio Ravara, Davide Sangiorgi, Vasco Thudichum Vasconcelos, and Gianluigi Zavattaro.","author":"Boreale Michele","year":"2006","unstructured":"Michele Boreale , Roberto Bruni , Lu\u00eds Caires , Rocco De Nicola , Ivan Lanese, Michele Loreti, Francisco Martins, Ugo Montanari, Ant\u00f3nio Ravara, Davide Sangiorgi, Vasco Thudichum Vasconcelos, and Gianluigi Zavattaro. 2006 . SCC : A service centered calculus. In WS-FM (LNCS), Vol. 4184 . Springer , Berlin, 38--57. Michele Boreale, Roberto Bruni, Lu\u00eds Caires, Rocco De Nicola, Ivan Lanese, Michele Loreti, Francisco Martins, Ugo Montanari, Ant\u00f3nio Ravara, Davide Sangiorgi, Vasco Thudichum Vasconcelos, and Gianluigi Zavattaro. 2006. SCC: A service centered calculus. In WS-FM (LNCS), Vol. 4184. Springer, Berlin, 38--57."},{"key":"e_1_2_1_26_1","volume-title":"Rocco De Nicola, and Michele Loreti","author":"Boreale Michele","year":"2008","unstructured":"Michele Boreale , Roberto Bruni , Rocco De Nicola, and Michele Loreti . 2008 . Sessions and pipelines for structured service programming. In FMOODS (LNCS), Vol. 5051 . Springer , Berlin, 19--38. Michele Boreale, Roberto Bruni, Rocco De Nicola, and Michele Loreti. 2008. Sessions and pipelines for structured service programming. In FMOODS (LNCS), Vol. 5051. Springer, Berlin, 19--38."},{"key":"e_1_2_1_27_1","volume-title":"ASIAN (LNCS)","author":"Boudol G\u00e9rard","unstructured":"G\u00e9rard Boudol . 1997. Typing the use of resources in a concurrent calculus . In ASIAN (LNCS) , Vol. 1345 . Springer , Berlin , 239--253. G\u00e9rard Boudol. 1997. Typing the use of resources in a concurrent calculus. In ASIAN (LNCS), Vol. 1345. Springer, Berlin, 239--253."},{"key":"e_1_2_1_28_1","volume-title":"Software Composition (LNCS)","author":"Bravetti Mario","unstructured":"Mario Bravetti and Gianluigi Zavattaro . 2007. Towards a unifying theory for choreography conformance and contract compliance . In Software Composition (LNCS) , Vol. 4829 . Springer , Berlin , 34--50. Mario Bravetti and Gianluigi Zavattaro. 2007. Towards a unifying theory for choreography conformance and contract compliance. In Software Composition (LNCS), Vol. 4829. Springer, Berlin, 34--50."},{"key":"e_1_2_1_29_1","volume-title":"WS-FM (LNCS)","author":"Bravetti Mario","unstructured":"Mario Bravetti and Gianluigi Zavattaro . 2008a. Contract compliance and choreography conformance in the presence of message queues . In WS-FM (LNCS) , Vol. 5387 . Springer , Berlin , 37--54. Mario Bravetti and Gianluigi Zavattaro. 2008a. Contract compliance and choreography conformance in the presence of message queues. In WS-FM (LNCS), Vol. 5387. Springer, Berlin, 37--54."},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.5555\/2366366.2366371"},{"key":"e_1_2_1_31_1","volume-title":"SFM (LNCS)","author":"Bravetti Mario","unstructured":"Mario Bravetti and Gianluigi Zavattaro . 2009a. Contract-based discovery and composition of web services . In SFM (LNCS) , Vol. 5569 . Springer , Berlin , 261--295. Mario Bravetti and Gianluigi Zavattaro. 2009a. Contract-based discovery and composition of web services. In SFM (LNCS), Vol. 5569. Springer, Berlin, 261--295."},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129509007658"},{"key":"e_1_2_1_33_1","volume-title":"Conformance Testing Methodologies and Architectures for OSI Protocols","author":"Brinksma Ed","unstructured":"Ed Brinksma , Giuseppe Scollo , and Chris Steenbergen . 1995. Lotos specifications, their implementations and their tests . In Conformance Testing Methodologies and Architectures for OSI Protocols . IEEE Computer Society , Washington, DC , 468--479. Ed Brinksma, Giuseppe Scollo, and Chris Steenbergen. 1995. Lotos specifications, their implementations and their tests. In Conformance Testing Methodologies and Architectures for OSI Protocols. IEEE Computer Society, Washington, DC, 468--479."},{"key":"e_1_2_1_34_1","volume-title":"AMAST (LNCS)","author":"Brogi Antonio","unstructured":"Antonio Brogi , Carlos Canal , and Ernesto Pimentel . 2004. Behavioural types and component adaptation . In AMAST (LNCS) , Vol. 3116 . Springer , Berlin , 42--56. Antonio Brogi, Carlos Canal, and Ernesto Pimentel. 2004. Behavioural types and component adaptation. In AMAST (LNCS), Vol. 3116. Springer, Berlin, 42--56."},{"key":"e_1_2_1_35_1","volume-title":"AMAST (LNCS)","author":"Bruni Roberto","unstructured":"Roberto Bruni and Leonardo Gaetano Mezzina . 2008. Types and deadlock freedom in a calculus of services, sessions and pipelines . In AMAST (LNCS) , Vol. 5140 . Springer , Berlin , 100--115. Roberto Bruni and Leonardo Gaetano Mezzina. 2008. Types and deadlock freedom in a calculus of services, sessions and pipelines. In AMAST (LNCS), Vol. 5140. Springer, Berlin, 100--115."},{"key":"e_1_2_1_36_1","volume-title":"Specification of realizable service conversations using collaboration diagrams","author":"Bultan Tevfik","unstructured":"Tevfik Bultan and Xiang Fu. 2007. Specification of realizable service conversations using collaboration diagrams . In SOCA. IEEE Computer Society , Washington, DC , 122--132. Tevfik Bultan and Xiang Fu. 2007. Specification of realizable service conversations using collaboration diagrams. In SOCA. IEEE Computer Society, Washington, DC, 122--132."},{"key":"e_1_2_1_37_1","volume-title":"ICSOC (LNCS)","author":"Busi Nadia","unstructured":"Nadia Busi , Roberto Gorrieri , Claudio Guidi , Roberto Lucchi , and Gianluigi Zavattaro . 2005. Choreography and orchestration: A synergic approach for system design . In ICSOC (LNCS) , Vol. 3826 . Springer , Berlin , 228--240. Nadia Busi, Roberto Gorrieri, Claudio Guidi, Roberto Lucchi, and Gianluigi Zavattaro. 2005. Choreography and orchestration: A synergic approach for system design. In ICSOC (LNCS), Vol. 3826. Springer, Berlin, 228--240."},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2008.04.030"},{"key":"e_1_2_1_39_1","volume-title":"ESOP (LNCS)","author":"Caires Lu\u00eds","unstructured":"Lu\u00eds Caires , Jorge A. P\u00e9rez , Frank Pfenning , and Bernardo Toninho . 2013. Behavioral polymorphism and parametricity in session-based communication . In ESOP (LNCS) , Vol. 7792 . Springer , Berlin , 330--349. Lu\u00eds Caires, Jorge A. P\u00e9rez, Frank Pfenning, and Bernardo Toninho. 2013. Behavioral polymorphism and parametricity in session-based communication. In ESOP (LNCS), Vol. 7792. Springer, Berlin, 330--349."},{"key":"e_1_2_1_40_1","volume-title":"CONCUR (LNCS)","author":"Caires Lu\u00eds","unstructured":"Lu\u00eds Caires and Frank Pfenning . 2010. Session types as intuitionistic linear propositions . In CONCUR (LNCS) , Vol. 6269 . Springer , Berlin , 222--236. Lu\u00eds Caires and Frank Pfenning. 2010. Session types as intuitionistic linear propositions. In CONCUR (LNCS), Vol. 6269. Springer, Berlin, 222--236."},{"key":"e_1_2_1_41_1","doi-asserted-by":"crossref","unstructured":"Lu\u00eds Caires Frank Pfenning and Bernardo Toninho. 2015. Linear logic propositions as session types. (unpublished). Lu\u00eds Caires Frank Pfenning and Bernardo Toninho. 2015. Linear logic propositions as session types. (unpublished).","DOI":"10.1017\/S0960129514000218"},{"key":"e_1_2_1_42_1","volume-title":"POPL","author":"Caires Lu\u00eds","unstructured":"Lu\u00eds Caires and Jo\u00e3o Costa Seco . 2013. The type discipline of behavioral separation . In POPL . ACM , New York, NY , 275--286. Lu\u00eds Caires and Jo\u00e3o Costa Seco. 2013. The type discipline of behavioral separation. In POPL. ACM, New York, NY, 275--286."},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2010.09.010"},{"key":"e_1_2_1_44_1","volume-title":"FSTTCS (LIPIcs)","volume":"8","author":"Capecchi Sara","year":"2010","unstructured":"Sara Capecchi , Elena Giachino , and Nobuko Yoshida . 2010 . Global escape in multiparty sessions . In FSTTCS (LIPIcs) , Vol. 8 . Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 338--351. Sara Capecchi, Elena Giachino, and Nobuko Yoshida. 2010. Global escape in multiparty sessions. In FSTTCS (LIPIcs), Vol. 8. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 338--351."},{"key":"e_1_2_1_45_1","volume-title":"PLACES (ENTCS)","author":"Carbone Marco","unstructured":"Marco Carbone . 2009. Session-based choreography with exceptions . In PLACES (ENTCS) . Elsevier , Amsterdam , 35--55. Marco Carbone. 2009. Session-based choreography with exceptions. In PLACES (ENTCS). Elsevier, Amsterdam, 35--55."},{"key":"e_1_2_1_46_1","volume-title":"CONCUR (LNCS)","author":"Carbone Marco","unstructured":"Marco Carbone , Kohei Honda , and Nobuko Yoshida . 2008. Structured interactional exceptions in session types . In CONCUR (LNCS) , Vol. 5201 . Springer , Berlin , 402--417. Marco Carbone, Kohei Honda, and Nobuko Yoshida. 2008. Structured interactional exceptions in session types. In CONCUR (LNCS), Vol. 5201. Springer, Berlin, 402--417."},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429101"},{"key":"e_1_2_1_48_1","volume-title":"WS-FM (LNCS)","author":"Carpineti Samuele","unstructured":"Samuele Carpineti , Giuseppe Castagna , Cosimo Laneve , and Luca Padovani . 2006. A formal account of contracts for web services . In WS-FM (LNCS) , Vol. 4184 . Springer , Berlin , 148--162. Samuele Carpineti, Giuseppe Castagna, Cosimo Laneve, and Luca Padovani. 2006. A formal account of contracts for web services. In WS-FM (LNCS), Vol. 4184. Springer, Berlin, 148--162."},{"key":"e_1_2_1_49_1","volume-title":"FORTE (LNCS)","author":"Carrez Cyril","unstructured":"Cyril Carrez , Alessandro Fantechi , and Elie Najm . 2003. Behavioural contracts for a sound assembly of components . In FORTE (LNCS) , Vol. 2767 . Springer , Berlin , 111--126. Cyril Carrez, Alessandro Fantechi, and Elie Najm. 2003. Behavioural contracts for a sound assembly of components. In FORTE (LNCS), Vol. 2767. Springer, Berlin, 111--126."},{"key":"e_1_2_1_50_1","volume-title":"PPDP","author":"Castagna Giuseppe","unstructured":"Giuseppe Castagna , Mariangiola Dezani-Ciancaglini , Elena Giachino , and Luca Padovani . 2009a. Foundations of session types . In PPDP . ACM , Berlin , 219--230. Giuseppe Castagna, Mariangiola Dezani-Ciancaglini, Elena Giachino, and Luca Padovani. 2009a. Foundations of session types. In PPDP. ACM, Berlin, 219--230."},{"key":"e_1_2_1_51_1","doi-asserted-by":"crossref","unstructured":"Giuseppe Castagna Mariangiola Dezani-Ciancaglini and Luca Padovani. 2012. On global types and multi-party sessions. Logical Methods Comput. Sci. 8 1 Article 24 45 pages. Giuseppe Castagna Mariangiola Dezani-Ciancaglini and Luca Padovani. 2012. On global types and multi-party sessions. Logical Methods Comput. Sci. 8 1 Article 24 45 pages.","DOI":"10.2168\/LMCS-8(1:24)2012"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538917.1538920"},{"key":"e_1_2_1_53_1","volume-title":"CONCUR (LNCS)","author":"Castagna Giuseppe","unstructured":"Giuseppe Castagna and Luca Padovani . 2009. Contracts for mobile processes . In CONCUR (LNCS) , Vol. 5710 . Springer , Berlin , 211--228. Giuseppe Castagna and Luca Padovani. 2009. Contracts for mobile processes. In CONCUR (LNCS), Vol. 5710. Springer, Berlin, 211--228."},{"key":"e_1_2_1_54_1","first-page":"265","article-title":"Formal verification of components assembly based on SysML and interface automata","volume":"7","author":"Chouali Samir","year":"2011","unstructured":"Samir Chouali and Ahmed Hammad . 2011 . Formal verification of components assembly based on SysML and interface automata . ISSE 7 , 4 (2011), 265 -- 274 . Samir Chouali and Ahmed Hammad. 2011. Formal verification of components assembly based on SysML and interface automata. ISSE 7, 4 (2011), 265--274.","journal-title":"ISSE"},{"key":"e_1_2_1_55_1","volume-title":"Adapting component behaviours using interface automata","author":"Chouali Samir","unstructured":"Samir Chouali , Sebti Mouelhi , and Hassan Mountassir . 2010. Adapting component behaviours using interface automata . In EUROMICRO-SEAA. IEEE Computer Society , Washington, DC , 119--122. Samir Chouali, Sebti Mouelhi, and Hassan Mountassir. 2010. Adapting component behaviours using interface automata. In EUROMICRO-SEAA. IEEE Computer Society, Washington, DC, 119--122."},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01211314"},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-0-387-35562-7_29"},{"key":"e_1_2_1_58_1","volume-title":"A set-constraint-based analysis of actors","author":"Cola\u00e7o Jean-Louis","unstructured":"Jean-Louis Cola\u00e7o , Mark Pantel , and Patrick Sall\u00e9 . 1997. A set-constraint-based analysis of actors . In FMOODS. Chapman & Hall , London , 1--16. Jean-Louis Cola\u00e7o, Mark Pantel, and Patrick Sall\u00e9. 1997. A set-constraint-based analysis of actors. In FMOODS. Chapman & Hall, London, 1--16."},{"key":"e_1_2_1_59_1","volume-title":"COORDINATION (LNCS)","author":"Coppo Mario","unstructured":"Mario Coppo , Mariangiola Dezani-Ciancaglini , Luca Padovani , and Nobuko Yoshida . 2013. Inference of global progress properties for dynamically interleaved multiparty sessions . In COORDINATION (LNCS) , Vol. 7890 . Springer , Berlin , 45--59. Mario Coppo, Mariangiola Dezani-Ciancaglini, Luca Padovani, and Nobuko Yoshida. 2013. Inference of global progress properties for dynamically interleaved multiparty sessions. In COORDINATION (LNCS), Vol. 7890. Springer, Berlin, 45--59."},{"key":"e_1_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129514000188"},{"key":"e_1_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(93)90086-9"},{"key":"e_1_2_1_62_1","volume-title":"FMOODS (LNCS)","author":"Cruz-Filipe Lu\u00eds","unstructured":"Lu\u00eds Cruz-Filipe , Ivan Lanese , Francisco Martins , Ant\u00f3nio Ravara , and Vasco Thudichum Vasconcelos . 2008. Behavioural theory at work: Program transformations in a service-centred calculus . In FMOODS (LNCS) , Vol. 5051 . Springer , Berlin , 59--77. Lu\u00eds Cruz-Filipe, Ivan Lanese, Francisco Martins, Ant\u00f3nio Ravara, and Vasco Thudichum Vasconcelos. 2008. Behavioural theory at work: Program transformations in a service-centred calculus. In FMOODS (LNCS), Vol. 5051. Springer, Berlin, 59--77."},{"key":"e_1_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-013-0284-5"},{"key":"e_1_2_1_64_1","volume-title":"PPDP","author":"Dardha Ornela","unstructured":"Ornela Dardha , Elena Giachino , and Davide Sangiorgi . 2012. Session types revisited . In PPDP . ACM , New York, NY , 139--150. Ornela Dardha, Elena Giachino, and Davide Sangiorgi. 2012. Session types revisited. In PPDP. ACM, New York, NY, 139--150."},{"key":"e_1_2_1_65_1","volume-title":"Henzinger","author":"de Alfaro Luca","year":"2001","unstructured":"Luca de Alfaro and Thomas A . Henzinger . 2001 . Interface automata. In ESEC-FSE. ACM, New York, NY , 109--120. Luca de Alfaro and Thomas A. Henzinger. 2001. Interface automata. In ESEC-FSE. ACM, New York, NY, 109--120."},{"key":"e_1_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(84)90113-0"},{"key":"e_1_2_1_67_1","volume-title":"ECOOP (LNCS)","author":"DeLine Robert","unstructured":"Robert DeLine and Manuel F\u00e4hndrich . 2004. Typestates for objects . In ECOOP (LNCS) , Vol. 3086 . Springer , Berlin , 465--490. Robert DeLine and Manuel F\u00e4hndrich. 2004. Typestates for objects. In ECOOP (LNCS), Vol. 3086. Springer, Berlin, 465--490."},{"key":"e_1_2_1_68_1","volume-title":"CONCUR (LNCS)","author":"Demangeon Romain","unstructured":"Romain Demangeon , Daniel Hirschkoff , and Davide Sangiorgi . 2010. Termination in impure concurrent languages . In CONCUR (LNCS) , Vol. 6269 . Springer , Berlin , 328--342. Romain Demangeon, Daniel Hirschkoff, and Davide Sangiorgi. 2010. Termination in impure concurrent languages. In CONCUR (LNCS), Vol. 6269. Springer, Berlin, 328--342."},{"key":"e_1_2_1_69_1","volume-title":"CONCUR (LNCS)","author":"Demangeon Romain","unstructured":"Romain Demangeon and Kohei Honda . 2011. Full abstraction in a subtyped pi-calculus with linear types . In CONCUR (LNCS) , Vol. 6901 . Springer , Berlin , 280--296. Romain Demangeon and Kohei Honda. 2011. Full abstraction in a subtyped pi-calculus with linear types. In CONCUR (LNCS), Vol. 6901. Springer, Berlin, 280--296."},{"key":"e_1_2_1_70_1","doi-asserted-by":"crossref","unstructured":"Pierre-Malo Deni\u00e9lou and Nobuko Yoshida. 2011. Dynamic multirole session types. In POPL. ACM 435--446. Pierre-Malo Deni\u00e9lou and Nobuko Yoshida. 2011. Dynamic multirole session types. In POPL. ACM 435--446.","DOI":"10.1145\/1925844.1926435"},{"key":"e_1_2_1_71_1","volume-title":"ICALP (2) (LNCS)","author":"Deni\u00e9lou Pierre-Malo","unstructured":"Pierre-Malo Deni\u00e9lou and Nobuko Yoshida . 2013. Multiparty compatibility in communicating automata: Characterisation and synthesis of global session types . In ICALP (2) (LNCS) , Vol. 7966 . Springer , Berlin , 174--186. Pierre-Malo Deni\u00e9lou and Nobuko Yoshida. 2013. Multiparty compatibility in communicating automata: Characterisation and synthesis of global session types. In ICALP (2) (LNCS), Vol. 7966. Springer, Berlin, 174--186."},{"key":"e_1_2_1_72_1","volume-title":"CSL (LIPIcs)","volume":"16","author":"DeYoung Henry","year":"2012","unstructured":"Henry DeYoung , Lu\u00eds Caires , Frank Pfenning , and Bernardo Toninho . 2012 . Cut reduction in linear logic as asynchronous session-typed communication . In CSL (LIPIcs) , Vol. 16 . Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 228--242. Henry DeYoung, Lu\u00eds Caires, Frank Pfenning, and Bernardo Toninho. 2012. Cut reduction in linear logic as asynchronous session-typed communication. In CSL (LIPIcs), Vol. 16. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 228--242."},{"key":"e_1_2_1_73_1","volume-title":"Ugo de\u2019Liguoro, and Nobuko Yoshida","author":"Dezani-Ciancaglini Mariangiola","year":"2007","unstructured":"Mariangiola Dezani-Ciancaglini , Ugo de\u2019Liguoro, and Nobuko Yoshida . 2007 . On progress for structured communications. In TGC (LNCS), Vol. 4912 . Springer , Berlin, 257--275. Mariangiola Dezani-Ciancaglini, Ugo de\u2019Liguoro, and Nobuko Yoshida. 2007. On progress for structured communications. In TGC (LNCS), Vol. 4912. Springer, Berlin, 257--275."},{"key":"e_1_2_1_74_1","volume-title":"FMCO (LNCS)","author":"Dezani-Ciancaglini Mariangiola","unstructured":"Mariangiola Dezani-Ciancaglini , Elena Giachino , Sophia Drossopoulou , and Nobuko Yoshida . 2006. Bounded session types for object oriented languages . In FMCO (LNCS) , Vol. 4709 . Springer , Berlin , 207--245. Mariangiola Dezani-Ciancaglini, Elena Giachino, Sophia Drossopoulou, and Nobuko Yoshida. 2006. Bounded session types for object oriented languages. In FMCO (LNCS), Vol. 4709. Springer, Berlin, 207--245."},{"key":"e_1_2_1_75_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2005.03.011"},{"key":"e_1_2_1_76_1","volume-title":"L-doos: A distributed object-oriented language with session types. In TGC (LNCS)","author":"Dezani-Ciancaglini Mariangiola","year":"2005","unstructured":"Mariangiola Dezani-Ciancaglini , Nobuko Yoshida , Alexander Ahern , and Sophia Drossopoulou . 2005 . L-doos: A distributed object-oriented language with session types. In TGC (LNCS) , Vol. 3705 . Springer , Berlin , 299--318. Mariangiola Dezani-Ciancaglini, Nobuko Yoshida, Alexander Ahern, and Sophia Drossopoulou. 2005. L-doos: A distributed object-oriented language with session types. In TGC (LNCS), Vol. 3705. Springer, Berlin, 299--318."},{"key":"e_1_2_1_77_1","volume-title":"ICFP","author":"Dunfield Joshua","unstructured":"Joshua Dunfield . 2012. Elaborating intersection and union types . In ICFP . ACM , New York, NY , 17--28. Joshua Dunfield. 2012. Elaborating intersection and union types. In ICFP. ACM, New York, NY, 17--28."},{"key":"e_1_2_1_78_1","volume-title":"FoSSaCS (LNCS)","author":"Dunfield Joshua","unstructured":"Joshua Dunfield and Frank Pfenning . 2003. Type assignment for intersections and unions in call-by-value languages . In FoSSaCS (LNCS) , Vol. 2620 . Springer , Berlin , 250--266. Joshua Dunfield and Frank Pfenning. 2003. Type assignment for intersections and unions in call-by-value languages. In FoSSaCS (LNCS), Vol. 2620. Springer, Berlin, 250--266."},{"key":"e_1_2_1_79_1","volume-title":"CAV (LNCS)","author":"Fournet C\u00e9dric","unstructured":"C\u00e9dric Fournet , C. A. R. Hoare , Sriram K. Rajamani , and Jakob Rehof . 2004. Stuck-free conformance . In CAV (LNCS) , Vol. 3114 . Springer , Berlin , 242--254. C\u00e9dric Fournet, C. A. R. Hoare, Sriram K. Rajamani, and Jakob Rehof. 2004. Stuck-free conformance. In CAV (LNCS), Vol. 3114. Springer, Berlin, 242--254."},{"key":"e_1_2_1_80_1","volume-title":"PLDI","author":"Freeman Tim","unstructured":"Tim Freeman and Frank Pfenning . 1991. Refinement types for ML . In PLDI . ACM , New York, NY , 268--277. Tim Freeman and Frank Pfenning. 1991. Refinement types for ML. In PLDI. ACM, New York, NY, 268--277."},{"key":"e_1_2_1_82_1","volume-title":"TGC (LNCS)","author":"Gamboni Maxime","unstructured":"Maxime Gamboni and Ant\u00f3nio Ravara . 2010. Responsive choice in mobile processes . In TGC (LNCS) , Vol. 6084 . Springer , Berlin , 135--152. Maxime Gamboni and Ant\u00f3nio Ravara. 2010. Responsive choice in mobile processes. In TGC (LNCS), Vol. 6084. Springer, Berlin, 135--152."},{"key":"e_1_2_1_83_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129508006944"},{"key":"e_1_2_1_84_1","first-page":"94","article-title":"Session types as generic process types","volume":"160","author":"Gay Simon J.","year":"2014","unstructured":"Simon J. Gay , Nils Gesbert , and Ant\u00f3nio Ravara . 2014 . Session types as generic process types . In EXPRESS\/SOS (EPTCS) , Vol. 160. 94 -- 110 . Simon J. Gay, Nils Gesbert, and Ant\u00f3nio Ravara. 2014. Session types as generic process types. In EXPRESS\/SOS (EPTCS), Vol. 160. 94--110.","journal-title":"EXPRESS\/SOS (EPTCS)"},{"key":"e_1_2_1_85_1","volume-title":"Gay and Malcolm Hole","author":"Simon","year":"1999","unstructured":"Simon J. Gay and Malcolm Hole . 1999 . Types and subtypes for client-server interactions. In ESOP (LNCS), Vol. 1576 . Springer , Berlin, 74--90. Simon J. Gay and Malcolm Hole. 1999. Types and subtypes for client-server interactions. In ESOP (LNCS), Vol. 1576. Springer, Berlin, 74--90."},{"key":"e_1_2_1_86_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-005-0177-z"},{"key":"e_1_2_1_87_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796809990268"},{"key":"e_1_2_1_88_1","volume-title":"Ant\u00f3nio Ravara, Nils Gesbert, and Alexandre Z. Caldeira.","author":"Gay Simon J.","year":"2010","unstructured":"Simon J. Gay , Vasco Thudichum Vasconcelos , Ant\u00f3nio Ravara, Nils Gesbert, and Alexandre Z. Caldeira. 2010 . Modular session types for distributed object-oriented programming. In POPL. ACM, New York, NY , 299--312. Simon J. Gay, Vasco Thudichum Vasconcelos, Ant\u00f3nio Ravara, Nils Gesbert, and Alexandre Z. Caldeira. 2010. Modular session types for distributed object-oriented programming. In POPL. ACM, New York, NY, 299--312."},{"key":"e_1_2_1_89_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90045-4"},{"key":"e_1_2_1_90_1","volume-title":"TAPSOFT(2) (LNCS)","author":"Girard Jean-Yves","unstructured":"Jean-Yves Girard and Yves Lafont . 1987. Linear logic and lazy computation . In TAPSOFT(2) (LNCS) , Vol. 250 . Springer , Berlin , 52--66. Jean-Yves Girard and Yves Lafont. 1987. Linear logic and lazy computation. In TAPSOFT(2) (LNCS), Vol. 250. Springer, Berlin, 52--66."},{"key":"e_1_2_1_91_1","volume-title":"WWV (EPTCS)","author":"Giunti Marco","unstructured":"Marco Giunti . 2011. A type checking algorithm for qualified session types . In WWV (EPTCS) , Vol. 61 . Open Publishing Association , 96--114. Marco Giunti. 2011. A type checking algorithm for qualified session types. In WWV (EPTCS), Vol. 61. Open Publishing Association, 96--114."},{"key":"e_1_2_1_92_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129514000176"},{"key":"e_1_2_1_93_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(02)00333-X"},{"key":"e_1_2_1_94_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129514000231"},{"key":"e_1_2_1_95_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0019-9958(84)80014-5"},{"key":"e_1_2_1_96_1","volume-title":"CONCUR (LNCS)","author":"Haack Christian","unstructured":"Christian Haack and Alan Jeffrey . 2005. Timed spi-calculus with types for secrecy and authenticity . In CONCUR (LNCS) , Vol. 3653 . Springer , Berlin , 202--216. Christian Haack and Alan Jeffrey. 2005. Timed spi-calculus with types for secrecy and authenticity. In CONCUR (LNCS), Vol. 3653. Springer, Berlin, 202--216."},{"key":"e_1_2_1_97_1","unstructured":"Carl Hewitt Peter Bishop and Richard Steiger. 1973. A universal modular actor formalism for artificial intelligence. In IJCAI. William Kaufmann 235--245. Carl Hewitt Peter Bishop and Richard Steiger. 1973. A universal modular actor formalism for artificial intelligence. In IJCAI. William Kaufmann 235--245."},{"key":"e_1_2_1_98_1","volume-title":"Communicating Sequential Processes","author":"Hoare C. A. R.","unstructured":"C. A. R. Hoare . 1985. Communicating Sequential Processes . Prentice-Hall , Upper Saddle River, NJ. C. A. R. Hoare. 1985. Communicating Sequential Processes. Prentice-Hall, Upper Saddle River, NJ."},{"key":"e_1_2_1_99_1","volume-title":"CONCUR (LNCS)","author":"Honda Kohei","unstructured":"Kohei Honda . 1993. Types for dyadic interaction . In CONCUR (LNCS) , Vol. 715 . Springer , Berlin , 509--523. Kohei Honda. 1993. Types for dyadic interaction. In CONCUR (LNCS), Vol. 715. Springer, Berlin, 509--523."},{"key":"e_1_2_1_100_1","volume-title":"Vasco Thudichum Vasconcelos, and Nobuko Yoshida","author":"Honda Kohei","year":"2012","unstructured":"Kohei Honda , Eduardo R. B. Marques , Francisco Martins , Nicholas Ng , Vasco Thudichum Vasconcelos, and Nobuko Yoshida . 2012 . Verification of MPI programs using session types. In EuroMPI (LNCS), Vol. 7490 . Springer , Berlin, 291--293. Kohei Honda, Eduardo R. B. Marques, Francisco Martins, Nicholas Ng, Vasco Thudichum Vasconcelos, and Nobuko Yoshida. 2012. Verification of MPI programs using session types. In EuroMPI (LNCS), Vol. 7490. Springer, Berlin, 291--293."},{"key":"e_1_2_1_101_1","volume-title":"Vasco Thudichum Vasconcelos, and Makoto Kubo","author":"Honda Kohei","year":"1998","unstructured":"Kohei Honda , Vasco Thudichum Vasconcelos, and Makoto Kubo . 1998 . Language primitives and type discipline for structured communication-based programming. In ESOP (LNCS), Vol. 1381 . Springer , Berlin, 122--138. Kohei Honda, Vasco Thudichum Vasconcelos, and Makoto Kubo. 1998. Language primitives and type discipline for structured communication-based programming. In ESOP (LNCS), Vol. 1381. Springer, Berlin, 122--138."},{"key":"e_1_2_1_102_1","volume-title":"POPL","author":"Honda Kohei","unstructured":"Kohei Honda , Nobuko Yoshida , and Marco Carbone . 2008. Multiparty asynchronous session types . In POPL . ACM , New York, NY , 273--284. Kohei Honda, Nobuko Yoshida, and Marco Carbone. 2008. Multiparty asynchronous session types. In POPL. ACM, New York, NY, 273--284."},{"key":"e_1_2_1_103_1","volume-title":"CONCUR (LNCS)","author":"H\u00fcttel Hans","unstructured":"Hans H\u00fcttel . 2011. Typed &psi;-calculi. In CONCUR (LNCS) , Vol. 6901 . Springer , Berlin , 265--279. Hans H\u00fcttel. 2011. Typed &psi;-calculi. In CONCUR (LNCS), Vol. 6901. Springer, Berlin, 265--279."},{"key":"e_1_2_1_104_1","volume-title":"TGC (LNCS)","author":"H\u00fcttel Hans","unstructured":"Hans H\u00fcttel . 2013. Types for resources in &psi;-calculi . In TGC (LNCS) , Vol. 8358 . Springer , Berlin , 83--102. Hans H\u00fcttel. 2013. Types for resources in &psi;-calculi. In TGC (LNCS), Vol. 8358. Springer, Berlin, 83--102."},{"key":"e_1_2_1_105_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2008.12.011"},{"key":"e_1_2_1_106_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2000.2872"},{"key":"e_1_2_1_107_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(03)00325-6"},{"key":"e_1_2_1_108_1","doi-asserted-by":"publisher","DOI":"10.5381\/jot.2007.6.2.a3"},{"key":"e_1_2_1_109_1","volume-title":"PLACES (EPTCS)","author":"Imai Keigo","unstructured":"Keigo Imai , Shoji Yuen , and Kiyoshi Agusa . 2010. Session type inference in Haskell . In PLACES (EPTCS) , Vol. 69 . Open Publishing Association , 74--91. Keigo Imai, Shoji Yuen, and Kiyoshi Agusa. 2010. Session type inference in Haskell. In PLACES (EPTCS), Vol. 69. Open Publishing Association, 74--91."},{"key":"e_1_2_1_111_1","doi-asserted-by":"publisher","DOI":"10.1145\/276393.278524"},{"key":"e_1_2_1_112_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44929-9_27"},{"key":"e_1_2_1_113_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0890-5401(02)93171-8"},{"key":"e_1_2_1_114_1","volume-title":"Formal Methods at the Crossroads. From Panacea to Foundational Support. LNCS","author":"Kobayashi Naoki","unstructured":"Naoki Kobayashi . 2003. Type systems for concurrent programs . In Formal Methods at the Crossroads. From Panacea to Foundational Support. LNCS , Vol. 2757 . Springer , Berlin , 439--453. Extended version available at http:\/\/www-kb.is.s.u-tokyo.ac.jp\/&sim;koba\/papers\/tutorial-type-extended.pdf. Naoki Kobayashi. 2003. Type systems for concurrent programs. In Formal Methods at the Crossroads. From Panacea to Foundational Support. LNCS, Vol. 2757. Springer, Berlin, 439--453. Extended version available at http:\/\/www-kb.is.s.u-tokyo.ac.jp\/&sim;koba\/papers\/tutorial-type-extended.pdf."},{"key":"e_1_2_1_115_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-005-0179-x"},{"key":"e_1_2_1_116_1","volume-title":"A type system equivalent to the modal mu-calculus model checking of higher-order recursion schemes","author":"Kobayashi Naoki","unstructured":"Naoki Kobayashi and C.-H. Luke Ong . 2009. A type system equivalent to the modal mu-calculus model checking of higher-order recursion schemes . In LICS. IEEE Computer Society , Washington, DC , 179--188. Naoki Kobayashi and C.-H. Luke Ong. 2009. A type system equivalent to the modal mu-calculus model checking of higher-order recursion schemes. In LICS. IEEE Computer Society, Washington, DC, 179--188."},{"key":"e_1_2_1_117_1","volume-title":"Turner","author":"Kobayashi Naoki","year":"1996","unstructured":"Naoki Kobayashi , Benjamin C. Pierce , and David N . Turner . 1996 . Linearity and the pi-calculus. In POPL. ACM, New York, NY , 358--371. Naoki Kobayashi, Benjamin C. Pierce, and David N. Turner. 1996. Linearity and the pi-calculus. In POPL. ACM, New York, NY, 358--371."},{"key":"e_1_2_1_118_1","doi-asserted-by":"publisher","DOI":"10.1145\/330249.330251"},{"key":"e_1_2_1_119_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44618-4_35"},{"key":"e_1_2_1_120_1","doi-asserted-by":"publisher","DOI":"10.1145\/1745312.1745313"},{"key":"e_1_2_1_121_1","doi-asserted-by":"publisher","DOI":"10.1017\/S096012951400019X"},{"key":"e_1_2_1_122_1","volume-title":"Bridging the gap between interaction- and process-oriented choreographies","author":"Lanese Ivan","unstructured":"Ivan Lanese , Claudio Guidi , Fabrizio Montesi , and Gianluigi Zavattaro . 2008. Bridging the gap between interaction- and process-oriented choreographies . In SEFM. IEEE Computer Society , Washington, DC , 323--332. Ivan Lanese, Claudio Guidi, Fabrizio Montesi, and Gianluigi Zavattaro. 2008. Bridging the gap between interaction- and process-oriented choreographies. In SEFM. IEEE Computer Society, Washington, DC, 323--332."},{"key":"e_1_2_1_123_1","volume-title":"Vasco Thudichum Vasconcelos, and Ant\u00f3nio Ravara","author":"Lanese Ivan","year":"2007","unstructured":"Ivan Lanese , Francisco Martins , Vasco Thudichum Vasconcelos, and Ant\u00f3nio Ravara . 2007 . Disciplining orchestration and conversation in service-oriented computing. In SEFM. IEEE Computer Society , Washington, DC, 305--314. Ivan Lanese, Francisco Martins, Vasco Thudichum Vasconcelos, and Ant\u00f3nio Ravara. 2007. Disciplining orchestration and conversation in service-oriented computing. In SEFM. IEEE Computer Society, Washington, DC, 305--314."},{"key":"e_1_2_1_124_1","volume-title":"WWV (EPTCS)","author":"Lanese Ivan","unstructured":"Ivan Lanese , Fabrizio Montesi , and Gianluigi Zavattaro . 2013. Amending choreographies . In WWV (EPTCS) , Vol. 123 . Open Publishing Association , 34--48. Ivan Lanese, Fabrizio Montesi, and Gianluigi Zavattaro. 2013. Amending choreographies. In WWV (EPTCS), Vol. 123. Open Publishing Association, 34--48."},{"key":"e_1_2_1_125_1","volume-title":"CONCUR (LNCS)","author":"Laneve Cosimo","unstructured":"Cosimo Laneve and Luca Padovani . 2007. The must preorder revisited . In CONCUR (LNCS) , Vol. 4703 . Springer , Berlin , 212--225. Cosimo Laneve and Luca Padovani. 2007. The must preorder revisited. In CONCUR (LNCS), Vol. 4703. Springer, Berlin, 212--225."},{"key":"e_1_2_1_126_1","volume-title":"IFM (LNCS)","author":"Laneve Cosimo","unstructured":"Cosimo Laneve and Luca Padovani . 2013. An algebraic theory for web service contracts . In IFM (LNCS) , Vol. 7940 . Springer , Berlin , 301--315. Cosimo Laneve and Luca Padovani. 2013. An algebraic theory for web service contracts. In IFM (LNCS), Vol. 7940. Springer, Berlin, 301--315."},{"key":"e_1_2_1_127_1","volume-title":"CONCUR (LNCS)","author":"Lange Julien","unstructured":"Julien Lange and Emilio Tuosto . 2012. Synthesising choreographies from local session types . In CONCUR (LNCS) , Vol. 7454 . Springer , 225--239. Julien Lange and Emilio Tuosto. 2012. Synthesising choreographies from local session types. In CONCUR (LNCS), Vol. 7454. Springer, 225--239."},{"key":"e_1_2_1_128_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-004-0043-8"},{"key":"e_1_2_1_129_1","doi-asserted-by":"publisher","DOI":"10.1145\/197320.197383"},{"key":"e_1_2_1_130_1","volume-title":"Vasco Thudichum Vasconcelos, and Nobuko Yoshida","author":"L\u00f3pez Hugo A.","year":"2015","unstructured":"Hugo A. L\u00f3pez , Eduardo R. B. Marques , Francisco Martins , Nicholas Ng , C\u00e9sar Santos , Vasco Thudichum Vasconcelos, and Nobuko Yoshida . 2015 . Protocol-based verification of message-passing parallel programs. In OOPSLA. ACM, New York, NY , 280--298. Hugo A. L\u00f3pez, Eduardo R. B. Marques, Francisco Martins, Nicholas Ng, C\u00e9sar Santos, Vasco Thudichum Vasconcelos, and Nobuko Yoshida. 2015. Protocol-based verification of message-passing parallel programs. In OOPSLA. ACM, New York, NY, 280--298."},{"key":"e_1_2_1_131_1","volume-title":"COORDINATION (LNCS)","author":"Mezzina Leonardo Gaetano","unstructured":"Leonardo Gaetano Mezzina . 2008. How to infer finite session types in a calculus of services and sessions . In COORDINATION (LNCS) , Vol. 5052 . Springer , Berlin , 216--231. Leonardo Gaetano Mezzina. 2008. How to infer finite session types in a calculus of services and sessions. In COORDINATION (LNCS), Vol. 5052. Springer, Berlin, 216--231."},{"key":"e_1_2_1_132_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129500001407"},{"key":"e_1_2_1_133_1","series-title":"NATO ASI Series","volume-title":"Logic and Algebra of Specification","author":"Milner Robin","unstructured":"Robin Milner . 1993. The polyadic &pi;-calculus: A tutorial . In Logic and Algebra of Specification . NATO ASI Series , Vol. 94 . Springer , Berlin , 203--246. Robin Milner. 1993. The polyadic &pi;-calculus: A tutorial. In Logic and Algebra of Specification. NATO ASI Series, Vol. 94. Springer, Berlin, 203--246."},{"key":"e_1_2_1_134_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(92)90008-4"},{"key":"e_1_2_1_135_1","volume-title":"CONCUR (LNCS)","author":"Montesi Fabrizio","unstructured":"Fabrizio Montesi and Nobuko Yoshida . 2013. Compositional choreographies . In CONCUR (LNCS) , Vol. 8052 . Springer , Berlin , 425--439. Fabrizio Montesi and Nobuko Yoshida. 2013. Compositional choreographies. In CONCUR (LNCS), Vol. 8052. Springer, Berlin, 425--439."},{"key":"e_1_2_1_136_1","volume-title":"TLCA (LNCS)","author":"Mostrous Dimitris","unstructured":"Dimitris Mostrous and Nobuko Yoshida . 2009. Session-based communication optimisation for higher-order mobile processes . In TLCA (LNCS) , Vol. 5608 . Springer , Berlin , 203--218. Dimitris Mostrous and Nobuko Yoshida. 2009. Session-based communication optimisation for higher-order mobile processes. In TLCA (LNCS), Vol. 5608. Springer, Berlin, 203--218."},{"key":"e_1_2_1_137_1","volume-title":"ESOP (LNCS)","author":"Mostrous Dimitris","unstructured":"Dimitris Mostrous , Nobuko Yoshida , and Kohei Honda . 2009. Global principal typing in partially commutative asynchronous sessions . In ESOP (LNCS) , Vol. 5502 . Springer , Berlin , 316--332. Dimitris Mostrous, Nobuko Yoshida, and Kohei Honda. 2009. Global principal typing in partially commutative asynchronous sessions. In ESOP (LNCS), Vol. 5502. Springer, Berlin, 316--332."},{"key":"e_1_2_1_138_1","volume-title":"ESOP (LNCS)","author":"Naik Mayur","unstructured":"Mayur Naik and Jens Palsberg . 2005. A type system equivalent to a model checker . In ESOP (LNCS) , Vol. 3444 . Springer , Berlin , 374--388. Mayur Naik and Jens Palsberg. 2005. A type system equivalent to a model checker. In ESOP (LNCS), Vol. 3444. Springer, Berlin, 374--388."},{"key":"e_1_2_1_139_1","volume-title":"A calculus of object bindings","author":"Najm Elie","unstructured":"Elie Najm and Abdelkrim Nimour . 1997. A calculus of object bindings . In FMOODS. Chapman & Hall , London . Elie Najm and Abdelkrim Nimour. 1997. A calculus of object bindings. In FMOODS. Chapman & Hall, London."},{"key":"e_1_2_1_140_1","volume-title":"FORTE (IFIP Conference Proceedings)","volume":"156","author":"Najm Elie","year":"1999","unstructured":"Elie Najm , Abdelkrim Nimour , and Jean-Bernard Stefani . 1999 a. Guaranteeing liveness in an object calculus through behavioural typing . In FORTE (IFIP Conference Proceedings) , Vol. 156 . Kluwer, Amsterdam, 203--221. Elie Najm, Abdelkrim Nimour, and Jean-Bernard Stefani. 1999a. Guaranteeing liveness in an object calculus through behavioural typing. In FORTE (IFIP Conference Proceedings), Vol. 156. Kluwer, Amsterdam, 203--221."},{"key":"e_1_2_1_141_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-0-387-35562-7_28"},{"key":"e_1_2_1_142_1","volume-title":"Pabble: Parameterised scribble for parallel programming","author":"Ng Nicholas","year":"2014","unstructured":"Nicholas Ng and Nobuko Yoshida . 2014 . Pabble: Parameterised scribble for parallel programming . In PDP. IEEE Computer Society , 707--714. Nicholas Ng and Nobuko Yoshida. 2014. Pabble: Parameterised scribble for parallel programming. In PDP. IEEE Computer Society, 707--714."},{"key":"e_1_2_1_143_1","volume-title":"CONCUR (LNCS)","author":"Nielson Flemming","unstructured":"Flemming Nielson and Hanne Riis Nielson . 1993. From CML to process algebras . In CONCUR (LNCS) , Vol. 715 . Springer , Berlin , 493--508. Flemming Nielson and Hanne Riis Nielson. 1993. From CML to process algebras. In CONCUR (LNCS), Vol. 715. Springer, Berlin, 493--508."},{"key":"e_1_2_1_144_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(95)00017-8"},{"key":"e_1_2_1_145_1","volume-title":"Hanne Riis Nielson, and Chris Hankin","author":"Nielson Flemming","year":"1999","unstructured":"Flemming Nielson , Hanne Riis Nielson, and Chris Hankin . 1999 . Principles of Program Analysis. Springer , Berlin. Flemming Nielson, Hanne Riis Nielson, and Chris Hankin. 1999. Principles of Program Analysis. Springer, Berlin."},{"key":"e_1_2_1_146_1","volume-title":"Object-Oriented Software Composition","author":"Nierstrasz Oscar","unstructured":"Oscar Nierstrasz . 1995. Regular types for active objects . In Object-Oriented Software Composition . Prentice Hall International , Upper Saddle River, NJ, 99--121. Oscar Nierstrasz. 1995. Regular types for active objects. In Object-Oriented Software Composition. Prentice Hall International, Upper Saddle River, NJ, 99--121."},{"key":"e_1_2_1_147_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2010.05.002"},{"key":"e_1_2_1_148_1","volume-title":"Session types &equals","author":"Padovani Luca","unstructured":"Luca Padovani . 2010b. Session types &equals ; intersection types + union types. In ITRS (EPTCS), Vol . 45. Open Publishing Association , 71--89. Luca Padovani. 2010b. Session types &equals; intersection types + union types. In ITRS (EPTCS), Vol. 45. Open Publishing Association, 71--89."},{"key":"e_1_2_1_149_1","volume-title":"COORDINATION (LNCS)","author":"Padovani Luca","unstructured":"Luca Padovani . 2011. Fair subtyping for multi-party session types . In COORDINATION (LNCS) , Vol. 6721 . Springer , Berlin , 127--141. Luca Padovani. 2011. Fair subtyping for multi-party session types. In COORDINATION (LNCS), Vol. 6721. Springer, Berlin, 127--141."},{"key":"e_1_2_1_150_1","volume-title":"ICALP (2) (LNCS)","author":"Padovani Luca","unstructured":"Luca Padovani . 2013a. Fair subtyping for open session types . In ICALP (2) (LNCS) , Vol. 7966 . Springer , Berlin , 373--384. Luca Padovani. 2013a. Fair subtyping for open session types. In ICALP (2) (LNCS), Vol. 7966. Springer, Berlin, 373--384."},{"key":"e_1_2_1_151_1","volume-title":"PLACES (EPTCS)","author":"Padovani Luca","unstructured":"Luca Padovani . 2013b. From lock freedom to progress using session types . In PLACES (EPTCS) , Vol. 137 . Open Publishing Association , 3--19. Luca Padovani. 2013b. From lock freedom to progress using session types. In PLACES (EPTCS), Vol. 137. Open Publishing Association, 3--19."},{"key":"e_1_2_1_152_1","first-page":"1","article-title":"Deadlock and lock freedom in the linear &pi;-calculus. In CSL-LICS. ACM, New York","volume":"72","author":"Padovani Luca","year":"2014","unstructured":"Luca Padovani . 2014 . Deadlock and lock freedom in the linear &pi;-calculus. In CSL-LICS. ACM, New York , NY , 72 : 1 -- 72 :10. Luca Padovani. 2014. Deadlock and lock freedom in the linear &pi;-calculus. In CSL-LICS. ACM, New York, NY, 72:1--72:10.","journal-title":"NY"},{"key":"e_1_2_1_153_1","volume-title":"CPP (LNCS)","author":"Pfenning Frank","unstructured":"Frank Pfenning , Lu\u00eds Caires , and Bernardo Toninho . 2011. Proof-carrying code in a session-typed process calculus . In CPP (LNCS) , Vol. 7086 . Springer , Berlin , 21--36. Frank Pfenning, Lu\u00eds Caires, and Bernardo Toninho. 2011. Proof-carrying code in a session-typed process calculus. In CPP (LNCS), Vol. 7086. Springer, Berlin, 21--36."},{"key":"e_1_2_1_155_1","doi-asserted-by":"publisher","DOI":"10.1017\/S096012950007002X"},{"key":"e_1_2_1_156_1","volume-title":"To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism","author":"Pottinger Garrel","unstructured":"Garrel Pottinger . 1980. A type assignment for the strongly normalizable lambda-terms . In To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism . Academic Press , New York, NY , 561--577. Garrel Pottinger. 1980. A type assignment for the strongly normalizable lambda-terms. In To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism. Academic Press, New York, NY, 561--577."},{"key":"e_1_2_1_157_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0096-0551(01)00019-4"},{"key":"e_1_2_1_158_1","doi-asserted-by":"publisher","DOI":"10.1002\/cpe.570"},{"key":"e_1_2_1_159_1","doi-asserted-by":"crossref","first-page":"315","DOI":"10.3233\/FUN-2001-48402","article-title":"Types for active objects with static deadlock prevention","volume":"48","author":"Puntigam Franz","year":"2001","unstructured":"Franz Puntigam and Christof Peter . 2001 . Types for active objects with static deadlock prevention . Fundam. Inform. 48 , 4 (2001), 315 -- 341 . Franz Puntigam and Christof Peter. 2001. Types for active objects with static deadlock prevention. Fundam. Inform. 48, 4 (2001), 315--341.","journal-title":"Fundam. Inform."},{"key":"e_1_2_1_160_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2011.12.005"},{"key":"e_1_2_1_161_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44618-4_34"},{"key":"e_1_2_1_162_1","volume-title":"Online Proceedings. 47--58","author":"Rehof Jakob","year":"2013","unstructured":"Jakob Rehof . 2013 . Towards combinatory logic synthesis. In BEAT , Online Proceedings. 47--58 . Jakob Rehof. 2013. Towards combinatory logic synthesis. In BEAT, Online Proceedings. 47--58."},{"key":"e_1_2_1_163_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2006.06.002"},{"key":"e_1_2_1_164_1","volume-title":"Algol-like Languages","author":"Reynolds John C.","unstructured":"John C. Reynolds . 1997. Design of the programming language Forsythe . In Algol-like Languages . Birkh\u00e4user , Basel , 173--233. John C. Reynolds. 1997. Design of the programming language Forsythe. In Algol-like Languages. Birkh\u00e4user, Basel, 173--233."},{"key":"e_1_2_1_165_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(96)00075-8"},{"key":"e_1_2_1_166_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1998.2711"},{"key":"e_1_2_1_167_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(99)00040-7"},{"key":"e_1_2_1_168_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129505004810"},{"key":"e_1_2_1_169_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1986.6312929"},{"key":"e_1_2_1_170_1","volume-title":"OOPSLA","author":"Sunshine Joshua","unstructured":"Joshua Sunshine , Karl Naden , Sven Stork , Jonathan Aldrich , and \u00c9ric Tanter . 2011. First-class state change in Plaid . In OOPSLA . ACM , New York, NY , 713--732. Joshua Sunshine, Karl Naden, Sven Stork, Jonathan Aldrich, and \u00c9ric Tanter. 2011. First-class state change in Plaid. In OOPSLA. ACM, New York, NY, 713--732."},{"key":"e_1_2_1_171_1","first-page":"34","article-title":"Principal type scheme for session types","volume":"3","author":"Tasistro Alvaro","year":"2012","unstructured":"Alvaro Tasistro , Ernesto Copello , and Nora Szasz . 2012 . Principal type scheme for session types . Int. J. Logic Comput. 3 , 1 (2012), 34 -- 43 . Alvaro Tasistro, Ernesto Copello, and Nora Szasz. 2012. Principal type scheme for session types. Int. J. Logic Comput. 3, 1 (2012), 34--43.","journal-title":"Int. J. Logic Comput."},{"key":"e_1_2_1_172_1","volume-title":"PPDP","author":"Toninho Bernardo","unstructured":"Bernardo Toninho , Lu\u00eds Caires , and Frank Pfenning . 2011. Dependent session types via intuitionistic linear type theory . In PPDP . ACM , New York, NY , 161--172. Bernardo Toninho, Lu\u00eds Caires, and Frank Pfenning. 2011. Dependent session types via intuitionistic linear type theory. In PPDP. ACM, New York, NY, 161--172."},{"key":"e_1_2_1_173_1","volume-title":"FoSSaCS (LNCS)","author":"Toninho Bernardo","unstructured":"Bernardo Toninho , Lu\u00eds Caires , and Frank Pfenning . 2012. Functions as session-typed processes . In FoSSaCS (LNCS) , Vol. 7213 . Springer , Berlin , 346--360. Bernardo Toninho, Lu\u00eds Caires, and Frank Pfenning. 2012. Functions as session-typed processes. In FoSSaCS (LNCS), Vol. 7213. Springer, Berlin, 346--360."},{"key":"e_1_2_1_174_1","volume-title":"ESOP (LNCS)","author":"Toninho Bernardo","unstructured":"Bernardo Toninho , Lu\u00eds Caires , and Frank Pfenning . 2013. Higher-order processes, functions, and sessions: A monadic integration . In ESOP (LNCS) , Vol. 7792 . Springer , Berlin , 350--369. Bernardo Toninho, Lu\u00eds Caires, and Frank Pfenning. 2013. Higher-order processes, functions, and sessions: A monadic integration. In ESOP (LNCS), Vol. 7792. Springer, Berlin, 350--369."},{"key":"e_1_2_1_175_1","first-page":"583","article-title":"Typing the behavior of software components using session types","volume":"73","author":"Vallecillo Antonio","year":"2006","unstructured":"Antonio Vallecillo , Vasco Thudichum Vasconcelos , and Ant\u00f3nio Ravara . 2006 . Typing the behavior of software components using session types . Fundam. Inform. 73 , 4 (2006), 583 -- 598 . Antonio Vallecillo, Vasco Thudichum Vasconcelos, and Ant\u00f3nio Ravara. 2006. Typing the behavior of software components using session types. Fundam. Inform. 73, 4 (2006), 583--598.","journal-title":"Fundam. Inform."},{"key":"e_1_2_1_176_1","volume-title":"ECOOP (LNCS)","author":"Vasconcelos Vasco Thudichum","unstructured":"Vasco Thudichum Vasconcelos . 1994. Typed concurrent objects . In ECOOP (LNCS) , Vol. 821 . Springer , Berlin , 100--117. Vasco Thudichum Vasconcelos. 1994. Typed concurrent objects. In ECOOP (LNCS), Vol. 821. Springer, Berlin, 100--117."},{"key":"e_1_2_1_177_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2012.05.002"},{"key":"e_1_2_1_178_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.06.028"},{"key":"e_1_2_1_179_1","volume-title":"ESOP (LNCS)","author":"Vieira Hugo Torres","unstructured":"Hugo Torres Vieira , Lu\u00eds Caires , and Jo\u00e3o Costa Seco . 2008. The conversation calculus: A model of service-oriented computation . In ESOP (LNCS) , Vol. 4960 . Springer , Berlin , 269--283. Hugo Torres Vieira, Lu\u00eds Caires, and Jo\u00e3o Costa Seco. 2008. The conversation calculus: A model of service-oriented computation. In ESOP (LNCS), Vol. 4960. Springer, Berlin, 269--283."},{"key":"e_1_2_1_180_1","volume-title":"COORDINATION (LNCS)","author":"Vieira Hugo Torres","unstructured":"Hugo Torres Vieira and Vasco Thudichum Vasconcelos . 2013. Typing progress in communication-centred systems . In COORDINATION (LNCS) , Vol. 7890 . Springer , Berlin , 236--250. Hugo Torres Vieira and Vasco Thudichum Vasconcelos. 2013. Typing progress in communication-centred systems. In COORDINATION (LNCS), Vol. 7890. Springer, Berlin, 236--250."},{"key":"e_1_2_1_181_1","unstructured":"Jules Villard. 2011. Heaps and Hops. Ph.D. Dissertation. ENS Cachan. Jules Villard. 2011. Heaps and Hops. Ph.D. Dissertation. ENS Cachan."},{"key":"e_1_2_1_182_1","volume-title":"ICFP","author":"Wadler Philip","unstructured":"Philip Wadler . 2012. Propositions as sessions . In ICFP . ACM , New York, NY , 273--286. Philip Wadler. 2012. Propositions as sessions. In ICFP. ACM, New York, NY, 273--286."},{"key":"e_1_2_1_183_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2003.08.004"},{"key":"e_1_2_1_184_1","volume-title":"FOSSACS (LNCS)","author":"Yoshida Nobuko","unstructured":"Nobuko Yoshida , Pierre-Malo Deni\u00e9lou , Andi Bejleri , and Raymond Hu. 2010. Parameterised multiparty session types . In FOSSACS (LNCS) , Vol. 6014 . Springer , Berlin , 128--145. Nobuko Yoshida, Pierre-Malo Deni\u00e9lou, Andi Bejleri, and Raymond Hu. 2010. Parameterised multiparty session types. In FOSSACS (LNCS), Vol. 6014. Springer, Berlin, 128--145."},{"key":"e_1_2_1_185_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2007.02.056"}],"container-title":["ACM Computing Surveys"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2873052","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2873052","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:53:49Z","timestamp":1750222429000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2873052"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,4,5]]},"references-count":181,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2017,3,31]]}},"alternative-id":["10.1145\/2873052"],"URL":"https:\/\/doi.org\/10.1145\/2873052","relation":{},"ISSN":["0360-0300","1557-7341"],"issn-type":[{"value":"0360-0300","type":"print"},{"value":"1557-7341","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,4,5]]},"assertion":[{"value":"2014-06-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2016-01-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2016-04-05","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}