An important goal of the BETTY meeting on 24 March is to obtain an overview of current research and to find out how to best collaborate within the network based on this overview.

Each WG1 member is encouraged to add up to 3 references (BibTeX format) to publications about foundational work on behavioural types that you think should be in our joint bibliography of important papers. Please also write a few lines about why you think this paper should be included and identify the theme. The papers do not have be ones that have you as an author.

If a topic within the area covered by WG1 is not represented by any current paper, mention the topic as a New keyword.

@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}, crossref = {DBLP:conf/popl/2013}, bibsource = {DBLP, http://dblp.uni-trier.de} }

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.

@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}, }

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} crossref = {DBLP:conf/popl/2010}, bibsource = {DBLP, http://dblp.uni-trier.de} }

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}}

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/tcs/IgarashiK04, author = {Atsushi Igarashi and Naoki Kobayashi}, title = {A generic type system for the Pi-calculus}, journal = {Theor. Comput. Sci.}, volume = {311}, number = {1-3}, year = {2004}, pages = {121-163}, ee = {http://dx.doi.org/10.1016/S0304-3975(03)00325-6}, bibsource = {DBLP, http://dblp.uni-trier.de} }

Justification: (by Luís Caires) This paper introduces a behavioural type system for the pi-calculus based on the idea approximating process behaviour by CCS process types, on which many interesting properties can be model-checked (as the type is finite state).

@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}}

Justification: (by Samir Chouali) The authors presented the use of interface automata to devise a behavioral type system for Ptolemy II (a software framework for concurrent component composition), that captures the 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 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}

Justification: (by Samir Chouali)In this paper, we proposed a method to enrich 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 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}

Justification: (by Samir Chouali) We presented a formal approach based on interface automata approach and protocols specifications, to adapt components in order to eliminate possible behavioural mismatches, that occur during their interactions. 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}

Justification: (by Samir Chouali) This paper describes an approach which combines component SysML models and interface automata in order to assemble components and to verify formally their interoperability. So, we proposed to verify formally 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}, crossref = {DBLP:conf/coordination/2012}, bibsource = {DBLP, http://dblp.uni-trier.de} }

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}, crossref = {DBLP:conf/concur/2012}, bibsource = {DBLP, http://dblp.uni-trier.de} }

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} }

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} }

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 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}, }

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.} }

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} }

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.} }

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} }

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}, }

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}, }

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}, }

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}, }

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}, }

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} }

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} }

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.

@inproceedings{DBLP:conf/ppdp/ToninhoCP11, author = {Bernardo Toninho and Lu\'{\i}s Caires and Frank Pfenning}, title = {Dependent session types via intuitionistic linear type theory}, booktitle = {PPDP}, year = {2011}, pages = {161-172}, ee = {http://doi.acm.org/10.1145/2003476.2003499}, crossref = {DBLP:conf/ppdp/2011}, bibsource = {DBLP, http://dblp.uni-trier.de} }

Justification: (by Bernardo Toninho) This paper extends Caires and Pfenning's CONCUR'10 paper to the setting of first-order (intuitionistic) linear logic, giving a robust and clean account of a system of (value) dependent session types, where processes may exchange channels, data and proof objects about the communicated data.

@inproceedings{DBLP:conf/fossacs/ToninhoCP12, author = {Bernardo Toninho and Lu\'{\i}s Caires and Frank Pfenning}, title = {Functions as Session-Typed Processes}, booktitle = {FoSSaCS}, year = {2012}, pages = {346-360}, ee = {http://dx.doi.org/10.1007/978-3-642-28729-9_23}, crossref = {DBLP:conf/fossacs/2012}, bibsource = {DBLP, http://dblp.uni-trier.de} }

Justification: (by Bernardo Toninho) This paper explores the logical interpretation of Caires and Pfenning's CONCUR'10 paper in the setting of concurrent evaluation strategies. By employing logically motivated translations from intuitionistic to linear logic (and thus from lambda to pi-calculus) copying and sharing concurrent reduction strategies are obtained.

@inproceedings{DBLP:conf/csl/DeYoungCPT12, author = {Henry DeYoung and Lu\'{\i}s Caires and Frank Pfenning and Bernardo Toninho}, title = {Cut Reduction in Linear Logic as Asynchronous Session-Typed Communication}, booktitle = {CSL}, year = {2012}, pages = {228-242}, ee = {http://dx.doi.org/10.4230/LIPIcs.CSL.2012.228}, crossref = {DBLP:conf/csl/2012}, bibsource = {DBLP, http://dblp.uni-trier.de} }

Justification: (by Bernardo Toninho) This paper explores an alternative process assignment to intuitionistic linear logic proofs to that of Caires and Pfenning's CONCUR'10 paper. The result is a system where the same proof rules are mapped to asynchronous processes in a faithful way, identifying asynchronous communication with proof reduction and a class of commuting conversions in logic as primitive structural equivalences.

@inproceedings{DBLP:conf/esop/CairesPPT13, author = {Lu\'{\i}s Caires and Jorge A. P{\'e}rez and Frank Pfenning and Bernardo Toninho}, title = {Behavioral Polymorphism and Parametricity in Session-Based Communication}, booktitle = {ESOP}, year = {2013}, pages = {330-349}, ee = {http://dx.doi.org/10.1007/978-3-642-37036-6_19}, crossref = {DBLP:conf/esop/2013}, bibsource = {DBLP, http://dblp.uni-trier.de} }

Justification: (by Luís Caires) This paper develops the behavioral theory of polymorphic session types, obtained via a process interpretation of second-order intuitionistic linear logic. In particular, it establishes a strong normalization and a relational parametricity result by employing the technique of linear logical relations developed in previous work by the authors, showing that the binary logical relation coincides with (typed) barbed congruence.

@inproceedings{DBLP:conf/esop/ToninhoCP13, author = {Bernardo Toninho and Lu\'{\i}s Caires and Frank Pfenning}, title = {Higher-Order Processes, Functions, and Sessions: A Monadic Integration}, booktitle = {ESOP}, year = {2013}, pages = {350-369}, ee = {http://dx.doi.org/10.1007/978-3-642-37036-6_20}, crossref = {DBLP:conf/esop/2013}, bibsource = {DBLP, http://dblp.uni-trier.de} }

Justification: (by Luís Caires) The paper presents a uniform integration of open session-typed processes and functional computation, motivated by logical considerations, in such a way that processes can reflect on functional terms and vice-versa. The result is a contextual concurrency monad that enables a very natural programming style with strong typing guarantees such as deadlock freedom, even in the presence of (typed) open higher-order processes.

@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} }

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, 7th European Symposium on Programming, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS'98, Lisbon, Portugal, March 28 - April 4, 1998, Proceedings}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = {1381}, isbn = {3-540-64302-8}, bibsource = {DBLP, http://dblp.uni-trier.de} }

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}, year = {1993}, isbn = {3-540-57208-2}, bibsource = {DBLP, http://dblp.uni-trier.de} }

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/parle/TakeuchiHK94, author = {Kaku Takeuchi and Kohei Honda and Makoto Kubo}, title = {An Interaction-based Language and its Typing System}, booktitle = {PARLE '94: Parallel Architectures and Languages Europe, 6th International PARLE Conference, Athens, Greece, July 4-8, 1994, Proceedings}, year = {1994}, pages = {398-413}, ee = {http://dx.doi.org/10.1007/3-540-58184-7_118}, crossref = {DBLP:conf/parle/1994}, bibsource = {DBLP, http://dblp.uni-trier.de} }

Justification: (by Luís Caires) Perhaps mostly interesting for historical reasons, this paper seems to be the very first proposal for a programming language encarnation of session types with all the usual modern features (results do not address delegation, although the type structure does) popularised by the Honda Vasconcelos and Kubo ESOP'98 paper.

@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}, crossref = {DBLP:conf/popl/2013}, bibsource = {DBLP, http://dblp.uni-trier.de} }

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}, crossref = {DBLP:conf/concur/2011}, bibsource = {DBLP, http://dblp.uni-trier.de} }

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{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}, crossref = {DBLP:conf/ppdp/2012}, bibsource = {DBLP, http://dblp.uni-trier.de} }

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}, }

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}, }

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

@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}, crossref = {DBLP:conf/ppdp/2009}, bibsource = {DBLP, http://dblp.uni-trier.de} }

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}, crossref = {DBLP:conf/ppdp/2012}, 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} }

Justification (by Hans Hüttel) This work presents a fully abstract translation of session types into a version of the simply typed pi-calculus.

@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}, } 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{, 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} }

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.

@inproceedings{DBLP:conf/popl/CairesS13, author = {Lu\'{\i}s Caires and Jo{\~a}o Costa Seco}, title = {The type discipline of behavioral separation}, booktitle = {The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '13, Rome, Italy - January 23 - 25, 2013}, year = {2013}, publisher = {ACM}, pages = {275-286}, ee = {http://doi.acm.org/10.1145/2429069.2429103}, bibsource = {DBLP, http://dblp.uni-trier.de} }

Justification: (by Luís Caires) Introduces behavioral separation types for disciplining interference in higher order concurrent imperative programs. Behavioral separation uses a behavioral type structure inspired in the separation logics. Well typed programs are race free and respect usage protocols.