{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,3]],"date-time":"2026-05-03T02:37:19Z","timestamp":1777775839248,"version":"3.51.4"},"reference-count":144,"publisher":"Emerald","issue":"2-3","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016,7,21]]},"abstract":"<jats:p>A recent trend in programming language research is to use behavioral type theory to ensure various correctness properties of large-scale, communication-intensive systems. Behavioral types encompass concepts such as interfaces, communication protocols, contracts, and choreography. The successful application of behavioral types requires a solid understanding of several practical aspects, from their representation in a concrete programming language, to their integration with other programming constructs such as methods and functions, to design and monitoring methodologies that take behaviors into account. This survey provides an overview of the state of the art of these aspects, which we summarize as the pragmatics of behavioral types.<\/jats:p>","DOI":"10.1561\/2500000031","type":"journal-article","created":{"date-parts":[[2016,7,21]],"date-time":"2016-07-21T04:33:37Z","timestamp":1469075617000},"page":"95-230","source":"Crossref","is-referenced-by-count":86,"title":["Behavioral Types in Programming Languages"],"prefix":"10.1108","volume":"3","author":[{"given":"Davide","family":"Ancona","sequence":"first","affiliation":[{"name":"Universit\u00e0 di Genova DIBRIS, ,","place":["Italy"]}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Viviana","family":"Bono","sequence":"additional","affiliation":[{"name":"Universit\u00e0 di Torino Dipartimento di Informatica, ,","place":["Italy"]}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mario","family":"Bravetti","sequence":"additional","affiliation":[{"name":"Universit\u00e0 di Bologna , Italy \/ INRIA,","place":["France"]}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Joana","family":"Campos","sequence":"additional","affiliation":[{"name":"Univ de Lisboa LaSIGE, Faculdade de Ci\u00eancias, ,","place":["Portugal"]}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Giuseppe","family":"Castagna","sequence":"additional","affiliation":[{"name":"Univ Paris Diderot CNRS, IRIF, , Sorbonne Paris Cit\u00e9,","place":["France"]}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pierre-Malo","family":"Deni\u00e9lou","sequence":"additional","affiliation":[{"name":"University of London Royal Holloway, ,","place":["UK"]}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Simon J.","family":"Gay","sequence":"additional","affiliation":[{"name":"University of Glasgow School of Computing Science, ,","place":["UK"]}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nils","family":"Gesbert","sequence":"additional","affiliation":[{"name":"Universit\u00e9 Grenoble Alpes ,","place":["France"]}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Elena","family":"Giachino","sequence":"additional","affiliation":[{"name":"Universit\u00e0 di Bologna , Italy \/ INRIA,","place":["France"]}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Raymond","family":"Hu","sequence":"additional","affiliation":[{"name":"Imperial College Department of Computing, London,","place":["UK"]}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Einar Broch","family":"Johnsen","sequence":"additional","affiliation":[{"name":"Universitetet i Oslo Institutt for informatikk, ,","place":["Norway"]}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Francisco","family":"Martins","sequence":"additional","affiliation":[{"name":"Univ de Lisboa LaSIGE, Faculdade de Ci\u00eancias, ,","place":["Portugal"]}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Viviana","family":"Mascardi","sequence":"additional","affiliation":[{"name":"Universit\u00e0 di Genova DIBRIS, ,","place":["Italy"]}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Fabrizio","family":"Montesi","sequence":"additional","affiliation":[{"name":"University of Southern Denmark"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rumyana","family":"Neykova","sequence":"additional","affiliation":[{"name":"Imperial College Department of Computing, London,","place":["UK"]}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nicholas","family":"Ng","sequence":"additional","affiliation":[{"name":"Imperial College Department of Computing, London,","place":["UK"]}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Luca","family":"Padovani","sequence":"additional","affiliation":[{"name":"Universit\u00e0 di Torino Dipartimento di Informatica, ,","place":["Italy"]}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Vasco T.","family":"Vasconcelos","sequence":"additional","affiliation":[{"name":"Univ de Lisboa LaSIGE, Faculdade de Ci\u00eancias, ,","place":["Portugal"]}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nobuko","family":"Yoshida","sequence":"additional","affiliation":[{"name":"Imperial College Department of Computing, London,","place":["UK"]}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"140","published-online":{"date-parts":[[2016,7,21]]},"reference":[{"key":"2026032910222430600_ref001","first-page":"1015","article-title":"Typestate-oriented programming","author":"Aldrich"},{"issue":"3","key":"2026032910222430600_ref002","doi-asserted-by":"crossref","first-page":"200","DOI":"10.4236\/jsea.2012.53026","article-title":"Privacy protection framework with defined policies for service-oriented architecture","volume":"5","author":"Allison","year":"2012","journal-title":"Journal of Software Engineering and Applications"},{"key":"2026032910222430600_ref003","first-page":"1","article-title":"Secure execution of distributed session programs","author":"Alves"},{"key":"2026032910222430600_ref004","first-page":"76","article-title":"Automatic Generation of Self-Monitoring MASs from Multiparty Global Session Types in Jason","author":"Ancona"},{"key":"2026032910222430600_ref005","first-page":"1377","article-title":"Constrained global types for dynamic checking of protocol conformance in multi-agent systems","author":"Ancona"},{"key":"2026032910222430600_ref006","doi-asserted-by":"crossref","DOI":"10.1145\/2480362.2480620","volume-title":"Global types for dynamic checking of protocol conformance in multi-agent systems","author":"Ancona","year":"2013"},{"key":"2026032910222430600_ref007","volume-title":"How to Do Things with Words","author":"Austin","year":"1962"},{"key":"2026032910222430600_ref008","first-page":"227","article-title":"Verifying correct usage of atomic blocks and typestate","author":"Beckman"},{"key":"2026032910222430600_ref009","doi-asserted-by":"crossref","DOI":"10.1002\/9780470058411","volume-title":"Developing Multi-Agent Systems with JADE","author":"Bellifemine","year":"2007"},{"key":"2026032910222430600_ref010","first-page":"61","article-title":"Mutually testing processes - (extended abstract)","author":"Bernardi"},{"key":"2026032910222430600_ref011","first-page":"659","volume-title":"Concurrency, Graphs and Models, volume 5065 of Lecture Notes in Computer Science","author":"Bettini","year":"2008"},{"key":"2026032910222430600_ref012","first-page":"418","article-title":"Global progress in dynamically interleaved multiparty sessions","author":"Bettini"},{"issue":"6","key":"2026032910222430600_ref013","doi-asserted-by":"crossref","first-page":"1163","DOI":"10.1017\/S0960129512000886","article-title":"Deriving session and union types for objects","volume":"23","author":"Bettini","year":"2013","journal-title":"Mathematical Structures in Computer Science"},{"key":"2026032910222430600_ref014","first-page":"124","article-title":"Cryptographic protocol synthesis and verification for multiparty sessions","author":"Bhargavan"},{"key":"2026032910222430600_ref015","first-page":"301","article-title":"Modular typestate checking of aliased objects","author":"Bierhoff"},{"key":"2026032910222430600_ref016","first-page":"50","article-title":"Monitoring networks through multiparty session types","author":"Bocchi"},{"key":"2026032910222430600_ref017","first-page":"419","article-title":"Timed multiparty session types","author":"Bocchi"},{"key":"2026032910222430600_ref018","first-page":"283","article-title":"Meeting deadlines together","author":"Bocchi"},{"key":"2026032910222430600_ref019","first-page":"1","article-title":"Typing Copyless Message Passing","volume":"8","author":"Bono","year":"2012","journal-title":"Logical Methods in Computer Science"},{"key":"2026032910222430600_ref020","first-page":"57","article-title":"Typing Copyless Message Passing","author":"Bono"},{"key":"2026032910222430600_ref021","first-page":"83","article-title":"Polymorphic Types for Leak Detection in a Session-Oriented Functional Language","author":"Bono"},{"key":"2026032910222430600_ref022","volume-title":"Programming Multi-Agent Systems in AgentSpeak Using Jason","author":"Bordini","year":"2007"},{"key":"2026032910222430600_ref023","first-page":"282","volume-title":"Results of the SENSORIA Project, volume 6582 of Lecture Notes in Computer Science","author":"Boreale","year":"2011"},{"key":"2026032910222430600_ref024","first-page":"55","article-title":"Checking interference with fractional permissions","author":"Boyland"},{"key":"2026032910222430600_ref025","first-page":"270","volume-title":"Aliasing in Object-Oriented Programming. Types, Analysis and Verification, volume 7850 of Lecture Notes in Computer Science","author":"Boyland","year":"2013"},{"key":"2026032910222430600_ref026","unstructured":"BPMN\n          . Business Process Model and Notation. http:\/\/www.omg.org\/spec\/BPMN\/2.0\/, 2011."},{"key":"2026032910222430600_ref027","doi-asserted-by":"crossref","first-page":"323","DOI":"10.1145\/322374.322380","article-title":"On communicating finite-state machines","volume":"30","author":"Brand","year":"1983","journal-title":"Journal of ACM"},{"key":"2026032910222430600_ref028","first-page":"34","volume-title":"Software Composition, volume 4829 of Lecture Notes in Computer Science","author":"Bravetti","year":"2007"},{"key":"2026032910222430600_ref029","first-page":"37","article-title":"Contract compliance and choreography conformance in the presence of message queues","author":"Bravetti"},{"issue":"4","key":"2026032910222430600_ref030","first-page":"451","article-title":"A foundational theory of contracts for multi-party service composition","volume":"89","author":"Bravetti","year":"2008","journal-title":"Fundamenta Informaticae"},{"key":"2026032910222430600_ref031","doi-asserted-by":"crossref","first-page":"60","DOI":"10.4018\/978-1-4666-2089-6.ch003","volume-title":"Adaptive Web Services for Modular and Reusable Software Development: Tactics and Solutions","author":"Bravetti","year":"2013"},{"key":"2026032910222430600_ref032","first-page":"222","article-title":"Session types as intuitionistic linear propositions","author":"Caires"},{"key":"2026032910222430600_ref033","unstructured":"Joana\n              Campos\n             and Vasco T.Vasconcelos. MOOL. Available at http:\/\/gloss.di.fc.ul.pt\/mool\/, accessedMay21, 2016."},{"key":"2026032910222430600_ref034","first-page":"12","article-title":"Channels as objects in concurrent object-oriented programming","author":"Campos"},{"key":"2026032910222430600_ref035","doi-asserted-by":"crossref","first-page":"142","DOI":"10.1016\/j.tcs.2008.09.016","article-title":"Amalgamating Sessions and Methods in Object Oriented Languages with Generics","volume":"410","author":"Capecchi","year":"2009","journal-title":"Theoretical Computer Science"},{"key":"2026032910222430600_ref036","first-page":"263","article-title":"Deadlock-freedom-by-design: multiparty asynchronous global programming","author":"Carbone"},{"key":"2026032910222430600_ref037","unstructured":"Marco\n              Carbone\n            , KoheiHonda, NobukoYoshida, RobinMilner, GaryBrown, and SteveRoss-Talbot. A theoretical basis of communication-centred concurrent programming, 2006. Available at http:\/\/www.w3.org\/2002\/ws\/chor\/edcopies\/theory\/note.pdf."},{"issue":"2","key":"2026032910222430600_ref038","doi-asserted-by":"crossref","first-page":"8","DOI":"10.1145\/2220365.2220367","article-title":"Structured communication-centered programming for web services","volume":"34","author":"Carbone","year":"2012","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"2026032910222430600_ref039","first-page":"47","article-title":"Choreographies, logically","author":"Carbone"},{"issue":"5","key":"2026032910222430600_ref040","doi-asserted-by":"crossref","DOI":"10.1145\/1538917.1538920","article-title":"A Theory of Contracts for Web Services","volume":"31","author":"Castagna","year":"2009","journal-title":"ACM Transactions on Programming Languages and Systems"},{"issue":"1","key":"2026032910222430600_ref041","article-title":"On global types and multi-party session","volume":"8","author":"Castagna","year":"2012","journal-title":"Logical Methods in Computer Science"},{"key":"2026032910222430600_ref042","unstructured":"CDL\n          . W3C Web Services Choreography Description Language. http:\/\/www.w3.org\/2002\/ws\/chor\/, 2002."},{"issue":"3","key":"2026032910222430600_ref043","doi-asserted-by":"crossref","first-page":"291","DOI":"10.1177\/1094342007078442","article-title":"Parallel pro-grammability and the chapel language","volume":"21","author":"Chamberlain","year":"2007","journal-title":"International Journal of High Performance Computing Applications"},{"key":"2026032910222430600_ref044","first-page":"519538","article-title":"X10: an object-oriented approach to non-uniform cluster computing","author":"Charles"},{"key":"2026032910222430600_ref045","first-page":"25","article-title":"Asynchronous distributed monitoring for multiparty session enforcement","author":"Chen"},{"key":"2026032910222430600_ref046","unstructured":"Chor\n          . Programming Language. Available at http:\/\/www.chor-lang.org\/, accessedMay21, 2016."},{"key":"2026032910222430600_ref047","first-page":"23","article-title":"VCC: A practical system for verifying concurrent C","author":"Cohen"},{"key":"2026032910222430600_ref048","first-page":"1","article-title":"Asynchronous Session Types and Progress for Object-Oriented Languages","author":"Coppo"},{"key":"2026032910222430600_ref049","first-page":"276","volume-title":"Trustworthy Global Computing, volume 4912 of Lecture Notes in Computer Science","author":"Corin","year":"2008"},{"issue":"5","key":"2026032910222430600_ref050","doi-asserted-by":"crossref","first-page":"573","DOI":"10.3233\/JCS-2008-0334","article-title":"A secure compiler for session abstractions","volume":"16","author":"Corin","year":"2008","journal-title":"Journal of Computer Security"},{"key":"2026032910222430600_ref051","first-page":"917","article-title":"The Chemical Approach to Typestate-Oriented Programming","author":"Crafa"},{"key":"2026032910222430600_ref052","first-page":"139","article-title":"Session types revisited","author":"Dardha"},{"key":"2026032910222430600_ref053","doi-asserted-by":"crossref","first-page":"83","DOI":"10.1016\/0304-3975(84)90113-0","article-title":"Testing equivalences for processes","volume":"34","author":"Nicola","year":"1984","journal-title":"Theoretical Computer Science"},{"key":"2026032910222430600_ref054","first-page":"465","article-title":"Typestates for objects","author":"DeLine"},{"key":"2026032910222430600_ref055","first-page":"272","article-title":"Nested protocols in session types","author":"Demangeon"},{"issue":"3","key":"2026032910222430600_ref056","doi-asserted-by":"crossref","first-page":"197","DOI":"10.1007\/s10703-014-0218-8","article-title":"Practical interruptible conversations: Distributed dynamic verification with multiparty session types and Python","volume":"46","author":"Demangeon","year":"2015","journal-title":"Formal Methods in System Design"},{"key":"2026032910222430600_ref057","first-page":"435","article-title":"Dynamic multirole session types","author":"Deni\u00e9lou"},{"key":"2026032910222430600_ref058","first-page":"194","article-title":"Multiparty session types meet communicating automata","author":"Deni\u00e9lou"},{"key":"2026032910222430600_ref059","first-page":"174","article-title":"Multiparty compatibility in communicating automata: Characterisation and synthesis of global session types","author":"Deni\u00e9lou"},{"issue":"4","key":"2026032910222430600_ref060","article-title":"Pa-rameterised multiparty session types","volume":"8","author":"Deni\u00e9lou","year":"2012","journal-title":"Logical Methods in Computer Science"},{"key":"2026032910222430600_ref061","unstructured":"Jolie development team\n          . Jolie Programming Language. Available athttp:\/\/www.jolie-lang.org\/, accessedMay21, 2016."},{"key":"2026032910222430600_ref062","first-page":"299","volume-title":"Trustworthy Global Computing, volume 3705 of Lecture Notes in Computer Science","author":"Dezani-Ciancaglini","year":"2005"},{"key":"2026032910222430600_ref063","first-page":"328","article-title":"Session Types for Object-Oriented Languages","author":"Dezani-Ciancaglini"},{"key":"2026032910222430600_ref064","first-page":"207","article-title":"Bounded Session Types for Object-Oriented Languages","author":"Dezani-Ciancaglini"},{"issue":"5","key":"2026032910222430600_ref065","doi-asserted-by":"crossref","first-page":"595","DOI":"10.1016\/j.ic.2008.03.028","article-title":"Objects and Session Types","volume":"207","author":"Dezani-Ciancaglini","year":"2009","journal-title":"Information and Computation"},{"key":"2026032910222430600_ref066","article-title":"Amalgamating the Session Types and the Object Oriented Programming Paradigms","author":"Drossopoulou"},{"key":"2026032910222430600_ref067","first-page":"13","article-title":"Adoption and focus: Practical linear types for imperative programming","author":"F\u00e4hndrich"},{"key":"2026032910222430600_ref068","first-page":"177","article-title":"Language Support for Fast and Reliable Message-based Communication in Singularity OS","author":"F\u00e4hndrich"},{"key":"2026032910222430600_ref069","volume-title":"MPI: A Message-Passing Interface Standard\u2014Version 3.0","author":"Forum","year":"2012"},{"key":"2026032910222430600_ref070","first-page":"112","article-title":"Multiparty session nets","author":"Fossati"},{"key":"2026032910222430600_ref071","unstructured":"Foundation for Intelligent Physical Agents\n          . FIPA ACL message structure specification. Available athttp:\/\/www.fipa.org\/specs\/fipa00061\/SC00061G.html, accessedMay21, 2016."},{"key":"2026032910222430600_ref072","first-page":"242","article-title":"Stuckfree conformance","author":"Fournet"},{"key":"2026032910222430600_ref073","doi-asserted-by":"crossref","DOI":"10.1145\/2629609","article-title":"Foundations of typestate-oriented programming","volume-title":"ACM Transactions on Programming Languages and Systems","author":"Garcia","year":"2014"},{"issue":"5","key":"2026032910222430600_ref074","doi-asserted-by":"crossref","first-page":"895","DOI":"10.1017\/S0960129508006944","article-title":"Bounded polymorphism in session types","volume":"18","author":"Gay","year":"2008","journal-title":"Mathematical Structures in Computer Science"},{"issue":"1","key":"2026032910222430600_ref075","doi-asserted-by":"crossref","first-page":"19","DOI":"10.1017\/S0956796809990268","article-title":"Linear type theory for asynchronous session types","volume":"20","author":"Gay","year":"2010","journal-title":"Journal of Functional Programming"},{"issue":"4","key":"2026032910222430600_ref076","article-title":"Modular session types for objects","volume":"11","author":"Gay","year":"2015","journal-title":"Logical Methods in Computer Science"},{"key":"2026032910222430600_ref077","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0304-3975(87)90045-4","article-title":"Linear logic","volume":"50","author":"Girard","year":"1987","journal-title":"Theoretical Computer Science"},{"key":"2026032910222430600_ref078","unstructured":"GMC\n          . From communicating machines to graphical choreographies. Available at https:\/\/bitbucket.org\/julien-lange\/gmc-synthesis, accessed21May2016."},{"key":"2026032910222430600_ref079","unstructured":"GTV\n          . Global Types Verification. Available at http:\/\/www.disi.unige.it\/person\/MascardiV\/Software\/globalTypes.html, accessed21May2016."},{"issue":"1","key":"2026032910222430600_ref080","doi-asserted-by":"crossref","first-page":"73","DOI":"10.3233\/FI-2009-143","article-title":"Dynamic error handling in service oriented applications","volume":"95","author":"Guidi","year":"2009","journal-title":"Fundamenta Infor-maticae"},{"key":"2026032910222430600_ref081","first-page":"273","article-title":"Multiparty Asynchronous Session Types","author":"Honda"},{"key":"2026032910222430600_ref082","first-page":"55","article-title":"Scribbling interactions with a formal foundation","author":"Honda"},{"key":"2026032910222430600_ref083","first-page":"291","article-title":"Verification of mpi programs using session types","author":"Honda"},{"key":"2026032910222430600_ref084","first-page":"105","volume-title":"Concurrent Objects and Beyond - Papers dedicated to Akinori Yonezawa on the Occasion of His 65th Birthday, volume 8665 of Lecture Notes in Computer Science","author":"Honda","year":"2014"},{"key":"2026032910222430600_ref085","first-page":"401","article-title":"Hybrid session verification through API generation","author":"Hu"},{"key":"2026032910222430600_ref086","first-page":"516","article-title":"Session-based distributed programming in java","author":"Hu"},{"key":"2026032910222430600_ref087","first-page":"329","article-title":"Type-safe eventful sessions in Java","author":"Hu"},{"key":"2026032910222430600_ref088","first-page":"130","article-title":"Practical Interruptible Conversations: Distributed Dynamic Verification with Session Types and Python","author":"Hu"},{"key":"2026032910222430600_ref089","volume-title":"An Overview of the Singularity Project","author":"Hunt","year":"2005"},{"key":"2026032910222430600_ref090","first-page":"74","article-title":"Session type inference in Haskell","author":"Imai"},{"key":"2026032910222430600_ref091","first-page":"151","article-title":"Exception Handling for Copyless Messaging","author":"Jak\u0161i\u0107"},{"key":"2026032910222430600_ref092","doi-asserted-by":"crossref","first-page":"22","DOI":"10.1016\/j.scico.2013.05.001","article-title":"Exception Handling for Copyless Messaging","volume":"84","author":"Jaksic","year":"2014","journal-title":"Science of Computer Programming"},{"issue":"1","key":"2026032910222430600_ref093","doi-asserted-by":"crossref","first-page":"7","DOI":"10.1023\/A:1010090405266","article-title":"A roadmap of agent research and development","volume":"1","author":"Jennings","year":"1998","journal-title":"Autonomous Agents and Multi-Agent Systems"},{"issue":"6","key":"2026032910222430600_ref094","first-page":"60","article-title":"Sawsdl: Semantic annotations for wsdl and xml schema","volume":"11","author":"Kopecky","year":"2007","journal-title":"IEEE Xplore: IEEE Internet Computing"},{"key":"2026032910222430600_ref095","unstructured":"Dimitrios\n              Kouzapas\n            , OrnelaDardha, RolyPerera, and Simon J.Gay. Mungo. http:\/\/www.dcs.gla.ac.uk\/research\/mungo, 2015."},{"key":"2026032910222430600_ref096","first-page":"323","article-title":"Bridging the gap between interaction- and process-oriented choreographies","author":"Lanese"},{"key":"2026032910222430600_ref097","first-page":"221","article-title":"From communicating machines to graphical choreographies","author":"Lange"},{"key":"2026032910222430600_ref098","first-page":"280","article-title":"Protocol-based verification of message-passing parallel programs","author":"L\u00f3pez"},{"key":"2026032910222430600_ref099","unstructured":"Eduardo R. B.\n              Marques\n            , FranciscoMartins, NicholasNg, C\u00e9sarSantos, Vasco T.Vasconcelos, and NobukoYoshida. Specification and verification of protocols for MPI programs. Available athttp:\/\/www.di.fc.ul.pt\/~vv\/papers\/marques.martins_specification-verification-mpi.pdf, 2013a."},{"key":"2026032910222430600_ref100","first-page":"103","article-title":"Towards deductive verification of MPI programs against session types","author":"Marques"},{"issue":"4-5-Online-Supplement","key":"2026032910222430600_ref101","article-title":"Attribute global types for dynamic checking of protocols in logic-based multiagent systems","volume":"13","author":"Mascardi","year":"2013","journal-title":"Theory and Practice of Logic Programming"},{"key":"2026032910222430600_ref102","first-page":"347","article-title":"Evaluation of KQML as an agent communication language","author":"Mayfield"},{"key":"2026032910222430600_ref103","first-page":"506","article-title":"From inter-organizational workflows to process execution: Generating bpel from ws-cdl","author":"Mendling"},{"key":"2026032910222430600_ref104","volume-title":"Design and implementation of a behaviorally typed programming system for web services","author":"Milit\u00e3o","year":"2016"},{"key":"2026032910222430600_ref105","article-title":"An exception aware behavioral type system for object-oriented programs","author":"Milit\u00e3o"},{"key":"2026032910222430600_ref106","first-page":"761","article-title":"Process-aware web programming with Jolie","author":"Montesi"},{"key":"2026032910222430600_ref107","volume-title":"Choreographic Programming","author":"Montesi","year":"2013"},{"key":"2026032910222430600_ref108","first-page":"425","article-title":"Compositional choreographies","author":"Montesi"},{"key":"2026032910222430600_ref109","first-page":"13","article-title":"Composing services with Jolie","author":"Montesi"},{"key":"2026032910222430600_ref110","first-page":"81","article-title":"Service-oriented programming with Jolie","author":"Montesi"},{"issue":"12","key":"2026032910222430600_ref111","doi-asserted-by":"crossref","first-page":"993","DOI":"10.1145\/359657.359659","article-title":"Using encryption for authentication in large networks of computers","volume":"21","author":"Needham","year":"1978","journal-title":"Communications of the ACM"},{"key":"2026032910222430600_ref112","first-page":"56","article-title":"An implementation of session types","author":"Neubauer"},{"key":"2026032910222430600_ref113","first-page":"131","article-title":"Multiparty session actors","author":"Neykova"},{"key":"2026032910222430600_ref114","first-page":"358","article-title":"SPY: Local Verification of Global Protocols","author":"Neykova"},{"issue":"3-4","key":"2026032910222430600_ref115","doi-asserted-by":"crossref","first-page":"269","DOI":"10.1007\/s11761-014-0172-8","article-title":"Pabble: parameterised Scribble","volume":"9","author":"Ng","year":"2015","journal-title":"Service Oriented Computing and Applications"},{"key":"2026032910222430600_ref116","first-page":"110","article-title":"Safe parallel programming with session java","author":"Ng"},{"key":"2026032910222430600_ref117","first-page":"202","article-title":"Multiparty session c: Safe parallel programming with message optimisation","author":"Ng"},{"key":"2026032910222430600_ref118","first-page":"212","article-title":"Protocols by default: Safe MPI code generation based on session types","author":"Ng"},{"key":"2026032910222430600_ref119","unstructured":"OASIS\n          . Web Services Business Process Execution Language. http:\/\/docs.oasis-open.org\/wsbpel\/2.0\/wsbpel-v2.0.html, 2007."},{"key":"2026032910222430600_ref120","unstructured":"Pabble-MPI\n          . MPI Generation Framework. Available athttps:\/\/github.com\/sessionc\/pabble-mpi, accessedMay21, 2016."},{"key":"2026032910222430600_ref121","first-page":"213","volume-title":"Contract-based Discovery and Adaptation of Web Services, volume 5569 of Lecture Notes in Computer Science","author":"Padovani","year":"2009"},{"key":"2026032910222430600_ref122","doi-asserted-by":"crossref","first-page":"3328","DOI":"10.1016\/j.tcs.2010.05.002","article-title":"Contract-Based Discovery of Web Services Modulo Simple Orchestrators","volume":"411","author":"Padovani","year":"2010","journal-title":"Theoretical Computer Science"},{"key":"2026032910222430600_ref123","volume-title":"A Simple Library Implementation of Binary Sessions","author":"Padovani","year":"2015"},{"key":"2026032910222430600_ref124","first-page":"25","article-title":"Haskell session types with (almost) no class","author":"Pucella"},{"key":"2026032910222430600_ref125","first-page":"973","article-title":"Towards the theoretical foundation of choreography","author":"Qiu"},{"key":"2026032910222430600_ref126","first-page":"42","article-title":"AgentSpeak(L): BDI agents speak out in a logical computable language","author":"Rao"},{"issue":"2","key":"2026032910222430600_ref127","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1016\/j.ic.2006.06.002","article-title":"Fair testing","volume":"205","author":"Rensink","year":"2007","journal-title":"Information and Computation"},{"key":"2026032910222430600_ref128","doi-asserted-by":"crossref","DOI":"10.1017\/9781316134924","volume-title":"The Pi-Calculus - a theory of mobile processes","author":"Sangiorgi","year":"2001"},{"key":"2026032910222430600_ref129","article-title":"The asynchronous partitioned global address space model","author":"Saraswat"},{"key":"2026032910222430600_ref130","unstructured":"Scribble\n          . Available athttp:\/\/www.scribble.org, accessedMay21, 2016."},{"key":"2026032910222430600_ref131","first-page":"2","article-title":"Gradual typing for objects","author":"Siek"},{"key":"2026032910222430600_ref132","unstructured":"Singularity OS\n          . Available athttp:\/\/singularity.codeplex.com\/, accessedMay21, 2016."},{"key":"2026032910222430600_ref133","unstructured":"SJ\n          . Session J. Available athttp:\/\/code.google.com\/p\/sessionj\/, accessedMay21, 2016."},{"key":"2026032910222430600_ref134","first-page":"1","article-title":"Parallel programming and parallel abstractions in fortress","author":"Steele"},{"key":"2026032910222430600_ref135","first-page":"13","article-title":"Analyzing Singularity Channel Contracts","author":"Stengel"},{"issue":"1","key":"2026032910222430600_ref136","doi-asserted-by":"crossref","first-page":"157","DOI":"10.1109\/TSE.1986.6312929","article-title":"Typestate: A programming language concept for enhancing software reliability","volume":"12","author":"Strom","year":"1986","journal-title":"IEEE Transactions on Software Engineering"},{"key":"2026032910222430600_ref137","first-page":"713","article-title":"First-class state change in Plaid","author":"Sunshine"},{"key":"2026032910222430600_ref138","first-page":"37","article-title":"Changing state in the Plaid language","author":"Sunshine"},{"key":"2026032910222430600_ref139","first-page":"350","article-title":"Higher-order processes, functions, and sessions: A monadic integration","author":"Toninho"},{"issue":"1-2","key":"2026032910222430600_ref140","doi-asserted-by":"crossref","first-page":"64","DOI":"10.1016\/j.tcs.2006.06.028","article-title":"Typechecking a multithreaded functional language with session types","volume":"368","author":"Vasconcelos","year":"2006","journal-title":"Theoretical Computer Science"},{"key":"2026032910222430600_ref141","first-page":"194","article-title":"Proving Copyless Message Passing","author":"Villard"},{"key":"2026032910222430600_ref142","first-page":"275","article-title":"Tracking Heaps That Hop with Heap-Hop","author":"Villard"},{"key":"2026032910222430600_ref143","first-page":"459","article-title":"Gradual typestate","author":"Wolff"},{"issue":"4","key":"2026032910222430600_ref144","doi-asserted-by":"crossref","first-page":"73","DOI":"10.1016\/j.entcs.2007.02.056","article-title":"Language primitives and type discipline for structured communication-based programming revisited: Two systems for higher-order session communication","volume":"171","author":"Yoshida","year":"2007","journal-title":"Electronic Notes in Theoretical Computer Science"}],"container-title":["Foundations and Trends\u00ae in Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.emerald.com\/ftpgl\/article-pdf\/3\/2-3\/95\/11025484\/2500000031en.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/www.emerald.com\/ftpgl\/article-pdf\/3\/2-3\/95\/11025484\/2500000031en.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,29]],"date-time":"2026-04-29T18:16:49Z","timestamp":1777486609000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.emerald.com\/ftpgl\/article\/3\/2-3\/95\/1326566\/Behavioral-Types-in-Programming-Languages"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,7,21]]},"references-count":144,"journal-issue":{"issue":"2-3","published-print":{"date-parts":[[2016,7,21]]}},"URL":"https:\/\/doi.org\/10.1561\/2500000031","relation":{},"ISSN":["2325-1107","2325-1131"],"issn-type":[{"value":"2325-1107","type":"print"},{"value":"2325-1131","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,7,21]]}}}