@article{Carbone:2012:SCP:2220365.2220367, author = {Carbone, Marco and Honda, Kohei and Yoshida, Nobuko}, title = {Structured Communication-Centered Programming for Web Services}, journal = {ACM Trans. Program. Lang. Syst.}, issue_date = {June 2012}, volume = {34}, number = {2}, month = jun, year = {2012}, issn = {0164-0925}, pages = {8:1--8:78}, articleno = {8}, numpages = {78}, url = {http://doi.acm.org/10.1145/2220365.2220367}, doi = {10.1145/2220365.2220367}, acmid = {2220367}, publisher = {ACM}, address = {New York, NY, USA}, keywords = {Communication, choreography, end-point projection, process calculi, session types, type system, web services}, } @Comment **Justification**: (by Mariangiola Dezani) This paper introduces global types as descriptions of whole conversation scenarios and relates them to session types. @inproceedings{DBLP:conf/popl/GayVRGC10, author = {Simon J. Gay and Vasco Thudichum Vasconcelos and Ant{\'o}nio Ravara and Nils Gesbert and Alexandre Z. Caldeira}, title = {Modular session types for distributed object-oriented programming}, booktitle = {POPL}, year = {2010}, pages = {299-312}, ee = {http://doi.acm.org/10.1145/1706299.1706335}, bibsource = {DBLP, http://dblp.uni-trier.de} } @Comment **Justification**: (by Mariangiola Dezani) An elegant unification of communication channels and their session types, distributed object-oriented programming, and a form of typestates supporting non-uniform objects, i.e. objects that dynamically change the set of available methods. @article{DBLP:journals/toplas/CastagnaGP09, author = {Giuseppe Castagna and Nils Gesbert and Luca Padovani}, title = {A theory of contracts for Web services}, journal = {ACM Trans. Program. Lang. Syst.}, volume = {31}, number = {5}, year = {2009}, ee = {http://doi.acm.org/10.1145/1538917.1538920}, bibsource = {DBLP, http://dblp.uni-trier.de}} @Comment **Justification**: (by Mariangiola Dezani) This paper devises a theory of contracts that formalizes the compatibility of a client with a service, and the safe replacement of a service with another service. @article{DBLP:journals/fac/LeeX04, author= {Edward A. Lee and Yuhong Xiong}, title = {A behavioral type system and its application in Ptolemy II}, journal = {Formal Asp. Comput.}, volume = {16},number={3}, year={2004}, pages={210-237}, ee=http://dx.doi.org/10.1007/s00165-004-0043-8}, bibsource={DBLP, http://dblp.uni-trier.de}} @Comment **Justification**: (by Samir Chouali) The authors presented the use of interface automata to devise a behavioral type system for Ptolemy @Comment II (a software framework for concurrent component composition), that captures the @Comment interaction dynamics in a component-based design environment. The interaction types and component behavior are described by interface automata, and type checking is done through automata @Comment composition. @inproceedings{mcm09:ip, author = {Mouelhi, Sebti and Chouali, Samir and Mountassir, Hassan}, title = {Refinement of Interface Automata Strengthened by Action Semantics}, booktitle = {FESCA'09 proceedings}, series = {ENTCS, Electronic Notes in Theoretical Computer Science}, volume = {253-1}, pages = {111--126}, doi = {10.1016/j.entcs.2009.09.031}, url = {http://dx.doi.org/10.1016/j.entcs.2009.09.031}, address = {York, United Kingdom}, year = 2009} @Comment **Justification**: (by Samir Chouali)In this paper, we proposed a method to enrich @Comment the interface automata formalism, which specifies components protocols, by the semantics of actions in order to verify components compatibility and components substitutability at the levels @Comment of signatures, semantics, and actions protocols. @inproceedings{cmm10:ip, author = {Chouali, Samir and Mouelhi, Sebti and Mountassir, Hassan}, title = {Adapting Components Behaviours using Interface Automata}, booktitle = {SEAA'10, 36th Euromicro Conference on Software Engineering and Advanced Applications}, pages = {119-122}, doi = {10.1109/SEAA.2010.34}, url = {http://dx.doi.org/10.1109/SEAA.2010.34}, publisher = {IEEE Computer Society Press}, address = {Lille, France}, month = sep, year = 2010} @Comment **Justification**: (by Samir Chouali) We presented a formal approach based on interface automata approach and protocols specifications, @Comment to adapt components in order to eliminate possible behavioural mismatches, that occur during their interactions. @Comment This approach insures reuse of components in diverse situations without affecting their codes. @article{ChoualiH11, author = {Chouali, Samir and Hammad, Ahmed}, title = {Formal verification of components assembly based on {SysML} and interface automata}, journal = {ISSE, Special issue of the International NASA Journal on Innovations in Systems and Software Engineering}, pages = {265--274}, doi = {10.1007/s11334-011-0170-3}, url = {http://dx.doi.org/10.1007/s11334-011-0170-3}, volume = 7, number = 4, publisher = {Springer}, month = sep, year = 2011} @Comment **Justification**: (by Samir Chouali) This paper describes an approach which combines @Comment component SysML models and interface automata in @Comment order to assemble components and to verify formally @Comment their interoperability. So, we proposed to verify formally @Comment the assembly of components specified with the expressive and the semi-formal systems modeling language, SysML. @inproceedings{DBLP:conf/coordination/BartolettiTZ12, author = {Massimo Bartoletti and Emilio Tuosto and Roberto Zunino}, title = {On the Realizability of Contracts in Dishonest Systems}, booktitle = {COORDINATION}, year = {2012}, pages = {245-260}, ee = {http://dx.doi.org/10.1007/978-3-642-30829-1_17}, bibsource = {DBLP, http://dblp.uni-trier.de} } @Comment **Justification**: (by Alceste Scalas) This paper presents a calculus of contracting systems, allowing distributed participants to advertise behavioural contracts, reach agreements and realise them (or choose not to - unlike in traditional approaches based on behavioural types). The paper introduces the notion of "honesty" (i.e. the ability of a participant to always realize its advertised contracts, in any context) and proves it to be undecidable. @inproceedings{DBLP:conf/concur/LangeT12, author = {Julien Lange and Emilio Tuosto}, title = {Synthesising Choreographies from Local Session Types}, booktitle = {CONCUR}, year = {2012}, pages = {225-239}, ee = {http://dx.doi.org/10.1007/978-3-642-32940-1_17}, bibsource = {DBLP, http://dblp.uni-trier.de} } @Comment **Justification**: (by Alceste Scalas) The paper proposes a typing systems which allows, under some conditions, to synthesise a choreography (i.e. a multiparty global type) from a set of local session types which describe end-point behaviours (i.e. local types). @article{DBLP:journals/corr/abs-1203-0780, author = {Giuseppe Castagna and Mariangiola Dezani-Ciancaglini and Luca Padovani}, title = {On Global Types and Multi-Party Session}, journal = {Logical Methods in Computer Science}, volume = {8}, number = {1}, year = {2012}, ee = {http://dx.doi.org/10.2168/LMCS-8(1:24)2012}, bibsource = {DBLP, http://dblp.uni-trier.de} } @Comment **Justification**: (by Alceste Scalas) The paper presents a new, streamlined language of global types equipped with a trace-based semantics, whose features and restrictions are semantically justified. The paper also provides an extensive comparison with related specification languages adopted in different communities. @article{DBLP:journals/acta/GayH05, author = {Simon J. Gay and Malcolm Hole}, title = {Subtyping for session types in the pi calculus}, journal = {Acta Inf.}, volume = {42}, number = {2-3}, year = {2005}, pages = {191-225}, ee = {http://dx.doi.org/10.1007/s00236-005-0177-z}, bibsource = {DBLP, http://dblp.uni-trier.de} } @Comment **Justification**: (by Ugo de'Liguoro) This is a seminal paper, that has opened a new perspective in the setting of session types. I understand subtyping as a way of giving semantics to session types and I have tried to develop this idea in the @Comment following work. @inproceedings{Barbanera-deLiguoro:PPDP10, number = {}, volume = {}, author = {Franco Barbanera and Ugo de' Liguoro}, series = {ACM SIGPLAN}, booktitle = {Proc. of PPDP'10}, tag = {ACM SIGPLAN Symposium PPDP'10}, localfile = {http://www.di.unito.it/~deligu/papers/BdL10draft.pdf}, title = "Two Notions of Sub-behaviour for Session-based Client/Server Systems", publisher = {ACM}, year = {2010}, pages = {155-164}, } @Comment **Justification**: (by Ugo de'Liguoro) Here we propose a refinement and a simplification of the behavioural semantics of session types, based on the concepts of compliance and sub-behaviour from the theory of web contracts. @InProceedings{ Padovani11c, author = {Luca Padovani}, title = {{F}air {S}ubtyping for {M}ulti-{P}arty {S}ession {T}ypes}, booktitle = {Proceedings of the 13th Conference on Coordination Models and Languages}, volume = {LNCS 6721}, year = {2011}, pages = {127-141}, url = {http://www.di.unito.it/~padovani/Papers/FairSessionTypes.pdf} , publisher = {Springer}, doi = {10.1007/978-3-642-21464-6\_9}, abstract = {The standard subtyping relation used in dyadic session type theories may compromise the liveness of multi-party sessions. In this paper we define a \emph{fair} subtyping relation for multi-party session types that preserves liveness, we relate it with the standard subtyping relation, and we give algorithms for deciding it. As a side effect, we provide an original and remarkably simple coinductive characterization of the fair testing preorder for nondeterministic, sequential processes consisting of internal choices of outputs and external choices of inputs.} } @Comment **Justification**: (by Ugo de'Liguoro) In my view this the most promising and intriguing way to extend the notion of subtyping from diadic to multiparty sessions. @InProceedings{ Padovani11b, author = {Luca Padovani}, title = {{S}ession {T}ypes = {I}ntersection {T}ypes + {U}nion {T}ypes}, booktitle = {Proceedings of the 5th Workshop on Intersection Types and Related Systems (ITRS'10)}, volume = {EPTCS 45}, year = {2011}, pages = {71-89}, url = {http://www.di.unito.it/~padovani/Papers/SessionIntersectionUnion.pdf} , abstract = {We propose a semantically grounded theory of session types which relies on intersection and union types. We argue that intersection and union types are natural candidates for modeling branching points in session types and we show that the resulting theory overcomes some important defects of related behavioral theories. In particular, intersections and unions provide a native solution to the problem of computing joins and meets of session types. Also, the subtyping relation turns out to be a pre-congruence, while this is not always the case in related behavioral theories.}, doi = {10.4204/EPTCS.45.6} } @Comment **Justification**: (by Luca Padovani) This work shows the connection between choice operators in session types and intersection and union types in conventional (i.e. non-behavioural) type systems. @InProceedings{ CastagnaPadovani09, author = {Giuseppe Castagna and Luca Padovani}, title = {{C}ontracts for {M}obile {P}rocesses}, booktitle = {Proceedings of the 20th International Conference on Concurrency Theory (CONCUR'09)}, year = {2009}, volume = {LNCS 5710}, pages = {211-228}, publisher = {Springer}, url = {http://www.di.unito.it/~padovani/Papers/ContractsMobileProcesses.pdf} , doi = {10.1007/978-3-642-04081-8\_15}, abstract = {Theories identifying well-formed systems of processes -- those that lack communication errors and enjoy strong properties such as deadlock freedom -- are based either on session types, which are inhabited by channels, or on contracts, which are inhabited by processes. Current session type theories impose overly restrictive disciplines while contract theories only work for networks with fixed topology. Here we fill the gap between the two approaches by defining a theory of contracts for so-called mobile processes, those whose communications may include delegations and channel references.} } @Comment **Justification**: (by Luca Padovani) This work explores a contract-based approach for the analysis of distributed systems with dynamic communication topologies. @article{DBLP:journals/iandc/Kobayashi02, author = {Naoki Kobayashi}, title = {A Type System for Lock-Free Processes}, journal = {Inf. Comput.}, volume = {177}, number = {2}, year = {2002}, pages = {122-159}, ee = {http://dx.doi.org/10.1006/inco.2002.3171}, bibsource = {DBLP, http://dblp.uni-trier.de} } @Comment **Justification**: (by Luca Padovani) This work shows how to use behavioural types (very similar to session types) to reason about global properties of systems, in particular lock-freedom. @inproceedings{SEFM08, author = {Lanese, I. and Guidi, C. and Montesi, F. and Zavattaro, G.}, title = {Bridging the Gap between Interaction- and Process-Oriented Choreographies}, booktitle = {Proc. of SEFM'08}, year = {2008}, pages = {323--332}, editor = {Antonio Cerone and Stefan Gruner}, publisher = {IEEE Computer Society Press}, } @Comment **Justification**: (by Ivan Lanese) This work shows that different conditions are needed to make a choreography (similar to a global type) projectable onto single participants according to whether the semantics is synchronous or asynchronous and, in the asynchronous case, on whether one is interested in the order of send, of receive, or of both. @inproceedings{bocchiDATA, author = {Bocchi, L. and Honda, K. and Tuosto, E. and Yoshida, N.}, title = {A Theory of Design-by-Contract for Distributed Multiparty Interactions}, booktitle = {Proc. of CONCUR 2010}, year = {2010}, pages = {162--176}, editor = {Paul Gastin and Fran\c{c}ois Laroussinie}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = {6269}, } @Comment **Justification**: (by Ivan Lanese) This work shows how to add data to the theory of choreographies. In particular the paper introduces assertions on the communicated values and invariants for recursion. @article{BocchiAMEND, author = {Laura Bocchi and Julien Lange and Emilio Tuosto}, title = {Three Algorithms and a Methodology for Amending Contracts for Choreographies}, journal = {Sci. Ann. Comp. Sci.}, volume = {22}, number = {1}, year = {2012}, pages = {61-104}, ee = {http://dx.doi.org/10.7561/SACS.2012.1.61}, bibsource = {DBLP, http://dblp.uni-trier.de}, } @Comment **Justification**: (by Emilio Tuosto) Designing well-formed choreographies in the framework introduced in~\cite{BocchiDATA} is not easy. We propose algorithms to help designers in their task, discuss their suitability, and sketch a methodology based on the proposed algorithms. @inproceedings{hondaPOPL, author = {Honda, K. and Yoshida, N. and Carbone, M.}, title = {Multiparty asynchronous session types}, booktitle = {Proc. of POPL'08}, year = {2008}, pages = {273--284}, ee = {http://doi.acm.org/10.1145/1328438.1328472}, bibsource = {DBLP, http://dblp.uni-trier.de}, OPTeditor = {George C. Necula and Philip Wadler}, publisher = {ACM Press}, } @Comment **Justification**: (by Ivan Lanese) This work extends the theory of projection from global types to endpoint types to the asynchronous case. @inproceedings{2008, volume = {5201}, author = {Bettini, Lorenzo and Coppo, Mario and D'Antoni, Loris and De Luca, Marco and Dezani-Ciancaglini, Mariangiola and Yoshida, Nobuko}, series = {LNCS}, booktitle = {CONCUR'08}, title = {Global Progress in Dynamically Interleaved Multiparty Sessions}, url = {http://www.di.unito.it/~dezani/papers/bcdddyshort.pdf}, publisher = {Springer}, year = {2008}, pages = {418-433}, } @Comment **Justification**: (by Mario Coppo) This paper introduces a type system to prove progress properties for a system in which sessions can be interleaved in the same processes allowing strong interactions between them. A new version of the paper with a revised and deeper notion of progress can be found in http://www.di.unito.it/~padovani/Papers/CoppoDezaniYoshidaPadovani13.pdf. @inproceedings{DBLP:conf/sac/BernardiH12, author = {Giovanni Bernardi and Matthew Hennessy}, title = {Modelling session types using contracts}, booktitle = {SAC}, year = {2012}, pages = {1941-1946}, ee = {http://doi.acm.org/10.1145/2245276.2232097}, bibsource = {DBLP, http://dblp.uni-trier.de} } @Comment **Justification**: (by Mario Coppo) An interesting paper about the comparisons of session types and contracts. @inproceedings{DBLP:conf/concur/CairesP10, author = {Lu\'{\i}s Caires and Frank Pfenning}, title = {Session Types as Intuitionistic Linear Propositions}, booktitle = {CONCUR'10}, year = {2010}, pages = {222-236}, ee = {http://dx.doi.org/10.1007/978-3-642-15375-4_16}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = {6269}, bibsource = {DBLP, http://dblp.uni-trier.de} } @Comment **Justification**: (by Jorge A. Perez) This paper develops a Curry-Howard interpretation between binary session types and linear logic propositions. As linearity is an important and recurring theme in (behavioral) type systems for process calculi, this paper may be one basis for setting clean, robust foundations for modern behavioral type systems. @article{DBLP:journals/tcs/CairesV10, author = {Lu\'{\i}s Caires and Hugo Torres Vieira}, title = {Conversation types}, journal = {Theor. Comput. Sci.}, volume = {411}, number = {51-52}, year = {2010}, pages = {4399-4440}, ee = {http://dx.doi.org/10.1016/j.tcs.2010.09.010}, bibsource = {DBLP, http://dblp.uni-trier.de} } @Comment **Justification**: (by Hugo Torres Vieira) In this paper we introduce a generalisation of session types for multiparty interaction, unifying "local" and "global" types at the same level in the type language and defining a way to distribute "slices" of the protocol in a compositional way, which allows us in particular to address conversations between an unanticipated number of participants. @inproceedings{DBLP:conf/esop/HondaVK98, author = {Kohei Honda and Vasco Thudichum Vasconcelos and Makoto Kubo}, title = {Language Primitives and Type Discipline for Structured Communication-Based Programming}, year = {1998}, pages = {122-138}, editor = {Chris Hankin}, booktitle = {Programming Languages and Systems - ESOP'98}, publisher = {Springer}, series = {LNCS}, volume = {1381}, isbn = {3-540-64302-8}, bibsource = {DBLP, http://dblp.uni-trier.de} } @Comment **Justification**: (by Hugo Torres Vieira) Even if there is no need to justify, this seminal paper led to the wide dissemination of session types. @inproceedings{DBLP:conf/concur/Honda93, author = "Kohei Honda", title = {Types for Dyadic Interaction}, year = 1993, pages = {509-523}, editor = {Eike Best}, booktitle = {CONCUR '93, 4th International Conference on Concurrency Theory, Hildesheim, Germany, August 23-26, 1993, Proceedings}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = {715}, isbn = {3-540-57208-2}, bibsource = {DBLP, http://dblp.uni-trier.de} } @Comment **Justification**: (by Hugo Torres Vieira) Again, I believe there should be no need to justify, as this paper introduced the base ideas for session types. @inproceedings{DBLP:conf/popl/CarboneM13, author = {Marco Carbone and Fabrizio Montesi}, title = {Deadlock-freedom-by-design: multiparty asynchronous global programming}, booktitle = {POPL}, year = {2013}, pages = {263-274}, ee = {http://doi.acm.org/10.1145/2429069.2429101}, bibsource = {DBLP, http://dblp.uni-trier.de} } @Comment **Justification**: (by Marco Carbone) //Global descriptions// have been successfully employed for the verification and implementation of communicating systems, respectively as protocol specifications and choreographies. This work brings these two practices together by proposing a purely-global programming model. We develop a typing discipline that verifies choreographies against protocol specifications, based on multiparty sessions. Exploiting the nature of global descriptions, our type system defines a new class of deadlock-free concurrent systems (deadlock-freedom-by- design), provides type inference, and supports session mobility. @inproceedings{DBLP:conf/concur/DemangeonH11, author = {Romain Demangeon and Kohei Honda}, title = {Full Abstraction in a Subtyped pi-Calculus with Linear Types}, booktitle = {CONCUR}, year = {2011}, pages = {280-296}, ee = {http://dx.doi.org/10.1007/978-3-642-23217-6_19}, bibsource = {DBLP, http://dblp.uni-trier.de} } @Comment **Justification**: (by Daniel Hirschkoff) This work establishes a relationship between (diadic) session types in the pi-calculus and standard type systems for pi. See also, on this topic, the Concur 11 paper by Demangeon and Honda. @inproceedings{DBLP:conf/sfm/BravettiZ09, author = {Mario Bravetti and Gianluigi Zavattaro}, title = {Contract-Based Discovery and Composition of Web Services}, booktitle = {Formal Methods for Web Services, 9th International School on Formal Methods for the Design of Computer, Communication, and Software Systems, SFM 2009}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = {5569}, year = {2009}, pages = {261-295}, ee = {http://dx.doi.org/10.1007/978-3-642-01918-0_7}, } @Comment **Justification**: (by Mario Bravetti) This work presents a foundational theory of behavioural contracts for multi-party service composition, focusing on contract refinement (coarsest subcontract relation) and its relationship with (fair) testing @inproceedings{DBLP:conf/soco/BravettiZ07, author = {Mario Bravetti and Gianluigi Zavattaro}, title = {Towards a Unifying Theory for Choreography Conformance and Contract Compliance}, booktitle = {Software Composition, 6th International Symposium, SC 2007, Braga, Portugal, March 24-25, 2007, Revised Selected Papers}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = {4829}, year = {2007}, pages = {34-50}, ee = {http://dx.doi.org/10.1007/978-3-540-77351-1_4}, } @Comment **Justification**: (by Mario Bravetti) This work presents a foundational theory of behavioural contracts for multi-party service composition, focusing on the conformance relation of a contract for a given role with respect to a (well-formed) choreography @incollection{huttel2011, year={2011}, isbn={978-3-642-23216-9}, booktitle={CONCUR 2011 – Concurrency Theory}, volume={6901}, series={Lecture Notes in Computer Science}, editor={Katoen, Joost-Pieter and König, Barbara}, doi={10.1007/978-3-642-23217-6_18}, title={Typed {$\Psi$}-calculi}, url={http://dx.doi.org/10.1007/978-3-642-23217-6_18}, publisher={Springer Berlin Heidelberg}, author={H{\"{u}}ttel, Hans}, pages={265-279} } @Comment **Justification**: (by Hans Hüttel) This work presents a general type system for psi-calculi that also allows for instantiations to type/effect systems, including a version of Gordon and Jeffrey's system for correspondence types. @inproceedings{DBLP:conf/ppdp/CastagnaDGP09, author = {Giuseppe Castagna and Mariangiola Dezani-Ciancaglini and Elena Giachino and Luca Padovani}, title = {Foundations of session types}, booktitle = {PPDP}, year = {2009}, pages = {219-230}, ee = {http://doi.acm.org/10.1145/1599410.1599437}, bibsource = {DBLP, http://dblp.uni-trier.de} } @Comment **Justification** (by Hans Hüttel) This work presents a general account of session types for a version of the pi-calculus. @inproceedings{DBLP:conf/ppdp/DardhaGS12, author = {Ornela Dardha and Elena Giachino and Davide Sangiorgi}, title = {Session types revisited}, booktitle = {PPDP}, year = {2012}, pages = {139-150}, ee = {http://doi.acm.org/10.1145/2370776.2370794}, bibsource = {DBLP, http://dblp.uni-trier.de} } @proceedings{DBLP:conf/ppdp/2012, editor = {Danny De Schreye and Gerda Janssens and Andy King}, title = {Principles and Practice of Declarative Programming, PPDP'12, Leuven, Belgium - September 19 - 21, 2012}, booktitle = {PPDP}, publisher = {ACM}, year = {2012}, isbn = {978-1-4503-1522-7}, ee = {http://dl.acm.org/citation.cfm?id=2370776}, bibsource = {DBLP, http://dblp.uni-trier.de} } @Misc{TV13, author = {Hugo Torres Vieira and Vasco Thudichum Vasconcelos}, title = {Typing Progress in Communication-Centred Systems}, howpublished = {Submitted for publication}, year = {2013} } @Comment **Justification** (by Hans Hüttel) This work presents a fully abstract translation of session types into a version of the simply typed pi-calculus. @Comment **Justification**: (by Daniel Hirschkoff) This work introduces a theory of subtyping for the pi-calculus, which allows the authors to related (diadic) session types to more standard typing constructs for the pi-calculus. See also, on this subject, Dardha, Giachino and Sangiorgi's PPDP'12 paper. @inproceedings{Castagna:2009:CMP:1611711.1611728, author = {Castagna, Giuseppe and Padovani, Luca}, title = {Contracts for Mobile Processes}, booktitle = {Proceedings of the 20th International Conference on Concurrency Theory}, series = {CONCUR 2009}, year = {2009}, isbn = {978-3-642-04080-1}, location = {Bologna, Italy}, pages = {211--228}, numpages = {18}, url = {http://dx.doi.org/10.1007/978-3-642-04081-8_15}, doi = {10.1007/978-3-642-04081-8_15}, acmid = {1611728}, publisher = {Springer-Verlag}, address = {Berlin, Heidelberg}, } @Comment **Justification:** (by Adrian Francalanza) Through an adapted testing-based equivalence, they provide a semantic way how to relate contracts, in terms of the eventual outcome (deadlock, success or indefinite progress) of every sub-component making up the contract. @incollection{brusas, year={2012}, isbn={978-3-642-30064-6}, booktitle={Trustworthy Global Computing}, volume={7173}, series={Lecture Notes in Computer Science}, editor={Bruni, Roberto and Sassone, Vladimiro}, doi={10.1007/978-3-642-30065-3_2}, title={Asynchronous Distributed Monitoring for Multiparty Session Enforcement}, url={http://dx.doi.org/10.1007/978-3-642-30065-3_2}, publisher={Springer Berlin Heidelberg}, author={Chen, Tzu-Chun and Bocchi, Laura and Deniélou, Pierre-Malo and Honda, Kohei and Yoshida, Nobuko}, pages={25-45} } @Comment **Justification:** (by Adrian Francalanza) mainly deals with how to correctly instrument monitors for enforcing session types in a distributed setting. They also provide specification of "located process conformance" to a monitor's specification using bisimulation equivalence.