 |
 |
Giuseppe Castagna ; Mariangiola Dezani-Ciancaglini ; Luca Padovani - On Global Types and Multi-Party Session
lmcs:773 - Logical Methods in Computer Science, March 15, 2012, Volume 8, Issue 1 - https://doi.org/10.2168/LMCS-8(1:24)2012On Global Types and Multi-Party SessionArticle
Authors: Giuseppe Castagna 
; Mariangiola Dezani-Ciancaglini ; Luca Padovani 0000-0003-0951-7535##NULL##0000-0001-9097-1297Giuseppe Castagna;Mariangiola Dezani-Ciancaglini;Luca Padovani
Global types are formal specifications that describe communication protocols in terms of their global interactions. We present a new, streamlined language of global types equipped with a trace-based semantics and whose features and restrictions are semantically justified. The multi-party sessions obtained projecting our global types enjoy a liveness property in addition to the traditional progress and are shown to be sound and complete with respect to the set of traces of the originating global type. Our notion of completeness is less demanding than the classical ones, allowing a multi-party session to leave out redundant traces from an underspecified global type. In addition to the technical content, we discuss some limitations of our language of global types and provide an extensive comparison with related specification languages adopted in different communities.
Source: arXiv.org:1203.0780
Volume: Volume 8, Issue 1
Published on: March 15, 2012
Imported on: July 4, 2011
Keywords: Computer Science - Programming Languages,F.1.2, F.3.3, H.3.5, H.5.3
Classifications
Mathematics Subject Classification 20201
Sources:
- [1] zbMATH Open.
Bibliographic References
62 Documents citing this article
- Elaine Li;Felix Stutz;Thomas Wies;Damien Zufferey, Lecture notes in computer science, Complete Multiparty Session Type Projection with Automata, pp. 350-373, 2023, 10.1007/978-3-031-37709-9_17, https://doi.org/10.1007/978-3-031-37709-9_17.
- Luc Edixhoven;Sung-Shik Jongmans;José Proença;Ilaria Castellani, 2023, Branching pomsets: Design, expressiveness and applications to choreographies, Journal of Logical and Algebraic Methods in Programming, 136, pp. 100919, 10.1016/j.jlamp.2023.100919, https://doi.org/10.1016/j.jlamp.2023.100919.
- Bas van den Heuvel;Jorge A. Pérez, 2022, A decentralized analysis of multiparty protocols, Science of Computer Programming, 222, pp. 102840, 10.1016/j.scico.2022.102840, https://doi.org/10.1016/j.scico.2022.102840.
- Felix Stutz;Damien Zufferey, 2022, Comparing Channel Restrictions of Communicating State Machines, High-level Message Sequence Charts, and Multiparty Session Types, arXiv (Cornell University), 370, pp. 194-212, 10.4204/eptcs.370.13.
- Ilaria Castellani;Mariangiola Dezani-Ciancaglini;Paola Giannini, 2022, Asynchronous Sessions with Input Races, arXiv (Cornell University), 356, pp. 12-23, 10.4204/eptcs.356.2.
- Luc Edixhoven;Sung-Shik Jongmans, Data Archiving and Networked Services (DANS), Realisability of Branching Pomsets, pp. 185-204, 2022, 10.1007/978-3-031-20872-0_11, https://ir.cwi.nl/pub/32636.
- Ruben Hamers;Erik Horlings;Sung-Shik Jongmans, 2022, The Discourje project: run-time verification of communication protocols in Clojure, International Journal on Software Tools for Technology Transfer, 24, 5, pp. 757-782, 10.1007/s10009-022-00674-y, https://doi.org/10.1007/s10009-022-00674-y.
- Davide Ancona;Luca Franceschini;Angelo Ferrando;Viviana Mascardi, 2021, RML: Theory and practice of a domain specific language for runtime verification, Science of Computer Programming, 205, pp. 102610, 10.1016/j.scico.2021.102610.
- Rupak Majumdar;Madhavan Mukund;Felix Stutz;Damien Zufferey, International Conference on Concurrency Theory, Generalising Projection in Asynchronous Multiparty Session Types., pp. 24-, 2021, 10.4230/lipics.concur.2021.35.
- Davide Ancona;Angelo Ferrando;Viviana Mascardi, 2020, Can determinism and compositionality coexist in RML?, arXiv (Cornell University), 322, pp. 13-32, 10.4204/eptcs.322.4.
- Davide Basile;Maurice H. ter Beek;Rosario Pugliese, 2020, Synthesis of Orchestrations and Choreographies: Bridging the Gap between Supervisory Control and Coordination of Services, DOAJ (DOAJ: Directory of Open Access Journals), 10.23638/lmcs-16(2:9)2020.
- Ruben Hamers;Sung-Shik Jongmans, Lecture notes in computer science, Discourje: Runtime Verification of Communication Protocols in Clojure, pp. 266-284, 2020, 10.1007/978-3-030-45190-5_15, https://doi.org/10.1007/978-3-030-45190-5_15.
- Rupak Majumdar;Nobuko Yoshida;Damien Zufferey, 2020, Multiparty motion coordination: from choreographies to robotics programs, Proceedings of the ACM on Programming Languages, 4, OOPSLA, pp. 1-30, 10.1145/3428202, https://doi.org/10.1145/3428202.
- Sung-Shik Jongmans;Nobuko Yoshida, Lecture notes in computer science, Exploring Type-Level Bisimilarity towards More Expressive Multiparty Session Types, pp. 251-279, 2020, 10.1007/978-3-030-44914-8_10, https://doi.org/10.1007/978-3-030-44914-8_10.
- Franco Barbanera;Ugo de'Liguoro;Rolf Hennicker, 2019, Connecting open systems of communicating finite state machines, Journal of Logical and Algebraic Methods in Programming, 109, pp. 100476, 10.1016/j.jlamp.2019.07.004, https://doi.org/10.1016/j.jlamp.2019.07.004.
- Maurizio Gabbrielli;Saverio Giallorenzo;Ivan Lanese;Jacopo Mauro, Guess Who’s Coming: Runtime Inclusion of Participants in Choreographies, pp. 118-138, 2019, 10.1007/978-3-030-31175-9_8, https://hal.inria.fr/hal-02376243.
- Rolf Hennicker, Role-Based Development of Dynamically Evolving Esembles, pp. 3-24, 2019, 10.1007/978-3-030-23220-7_1, https://hal.inria.fr/hal-02364578.
- Rolf Hennicker;Martin Wirsing, Lecture notes in computer science, A Generic Dynamic Logic with Applications to Interaction-Based Systems, pp. 172-187, 2019, 10.1007/978-3-030-30985-5_11.
- Angelo Ferrando, 2018, The early bird catches the worm: First verify, then monitor!, Science of Computer Programming, 172, pp. 160-179, 10.1016/j.scico.2018.11.008, https://doi.org/10.1016/j.scico.2018.11.008.
- Davide Ancona;Angelo Ferrando;Luca Franceschini;Viviana Mascardi, Lecture notes in computer science, Coping with Bad Agent Interaction Protocols When Monitoring Partially Observable Multiagent Systems, pp. 59-71, 2018, 10.1007/978-3-319-94580-4_5.
- Gul Agha;Minas Charalambides;Kirill Mechitov;Karl Palmskog;Atul Sandur;et al., 2018, Theoretical Considerations: Inferring and Enforcing Use Patterns for Mobile Cloud Assurance, Assured Cloud Computing, pp. 237-276, 10.1002/9781119428497.ch7.
- Luca Padovani, 2018, A type checking algorithm for concurrent object protocols, Journal of Logical and Algebraic Methods in Programming, 100, pp. 16-35, 10.1016/j.jlamp.2018.06.001, https://doi.org/10.1016/j.jlamp.2018.06.001.
- Rolf Hennicker;Martin Wirsing, Lecture notes in computer science, Dynamic Logic for Ensembles, pp. 32-47, 2018, 10.1007/978-3-030-03424-5_3.
- Emilio Tuosto;Roberto Guanciale, 2017, Semantics of global view of choreographies, Journal of Logical and Algebraic Methods in Programming, 95, pp. 17-40, 10.1016/j.jlamp.2017.11.002, https://doi.org/10.1016/j.jlamp.2017.11.002.
- Ilaria Castellani;Mariangiola Dezani-Ciancaglini;Paola Giannini, Concurrent Reversible Sessions, 2017, 10.4230/lipics.concur.2017.30, https://hal.inria.fr/hal-01639845.
- Davide Ancona;Angelo Ferrando;Viviana Mascardi, Lecture notes in computer science, Comparing Trace Expressions and Linear Temporal Logic for Runtime Verification, pp. 47-64, 2016, 10.1007/978-3-319-30734-3_6.
- Hans Hüttel;Ivan Lanese;Vasco T. Vasconcelos;Luís Caires;Marco Carbone;et al., 2016, Foundations of Session Types and Behavioural Contracts, ACM Computing Surveys, 49, 1, pp. 1-36, 10.1145/2873052, https://doi.org/10.1145/2873052.
- Hugo A. López;Flemming Nielson;Hanne Riis Nielson, Enforcing Availability in Failure-Aware Communicating Systems, pp. 195-211, 2016, 10.1007/978-3-319-39570-8_13, https://hal.inria.fr/hal-01432918.
- Marco Carbone;Fabrizio Montesi;Carsten Schürmann;Nobuko Yoshida, 2016, Multiparty session types as coherence proofs, Acta Informatica, 54, 3, pp. 243-269, 10.1007/s00236-016-0285-y, https://doi.org/10.1007/s00236-016-0285-y.
- Roberto Guanciale;Emilio Tuosto, 2016, An Abstract Semantics of the Global View of Choreographies, arXiv (Cornell University), 223, pp. 67-82, 10.4204/eptcs.223.5.
- Alberto Lluch Lafuente;Flemming Nielson;Hanne Riis Nielson, Technical University of Denmark, DTU Orbit (Technical University of Denmark, DTU), Discretionary Information Flow Control for Interaction-Oriented Specifications, pp. 427-450, 2015, 10.1007/978-3-319-23165-5_20, https://orbit.dtu.dk/en/publications/5fa21f34-5eeb-407d-9dd7-80a523ff91cf.
- Davide Ancona;Daniela Briola;Angelo Ferrando;Viviana Mascardi, 2015, Runtime verification of fail-uncontrolled and ambient intelligence systems: A uniform approach, Intelligenza Artificiale, 9, 2, pp. 131-148, 10.3233/ia-150084.
- Ivan Lanese;Fabrizio Montesi;Gianluigi Zavattaro, The Evolution of Jolie, pp. 506-521, 2015, 10.1007/978-3-319-15545-6_29, https://hal.inria.fr/hal-01227623.
- Julien Lange;Emilio Tuosto;Nobuko Yoshida, 2015, From Communicating Machines to Graphical Choreographies, OPAL (Open@LaTrobe) (La Trobe University), 50, 1, pp. 221-232, 10.1145/2775051.2676964, https://figshare.com/articles/conference_contribution/From_Communicating_Machines_to_Graphical_Choreographies/10167236.
- Mario Coppo;Mariangiola Dezani-Ciancaglini;Luca Padovani;Nobuko Yoshida, Spiral (Imperial College London), A Gentle Introduction to Multiparty Asynchronous Session Types, pp. 146-178, 2015, 10.1007/978-3-319-18941-3_4, http://hdl.handle.net/10044/1/27022.
- Massimo Bartoletti;Maurizio Murgia;Alceste Scalas;Roberto Zunino, 2015, Verifiable abstractions for contract-oriented systems, Journal of Logical and Algebraic Methods in Programming, 86, 1, pp. 159-207, 10.1016/j.jlamp.2015.10.005, https://doi.org/10.1016/j.jlamp.2015.10.005.
- Mila Dalla Preda;Maurizio Gabbrielli;Saverio Giallorenzo;Ivan Lanese;Jacopo Mauro, Lecture notes in computer science, Dynamic Choreographies, pp. 67-82, 2015, 10.1007/978-3-319-19282-6_5, https://doi.org/10.1007/978-3-319-19282-6_5.
- Minas Charalambides;Peter Dinges;Gul Agha, 2015, Parameterized, concurrent session types for asynchronous multi-actor interactions, Science of Computer Programming, 115-116, pp. 100-126, 10.1016/j.scico.2015.10.006.
- Tzu-Chun Chen, 2015, Lightening global types, Journal of Logical and Algebraic Methods in Programming, 84, 5, pp. 708-729, 10.1016/j.jlamp.2015.06.003, https://doi.org/10.1016/j.jlamp.2015.06.003.
- Davide Ancona;Daniela Briola;Amal El Fallah Seghrouchni;Viviana Mascardi;Patrick Taillibert, CiteSeer X (The Pennsylvania State University), Efficient Verification of MASs with Projections, pp. 246-270, 2014, 10.1007/978-3-319-14484-9_13, http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.712.6426.
- Davide Basile;Pierpaolo Degano;Gian Luigi Ferrari, CiteSeer X (The Pennsylvania State University), Automata for Analysing Service Contracts, pp. 34-50, 2014, 10.1007/978-3-662-45917-1_3, http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.640.5123.
- Julien Lange;Emilio Tuosto;Nobuko Yoshida, OPAL (Open@LaTrobe) (La Trobe University), From Communicating Machines to Graphical Choreographies, pp. 221-232, 2014, Mumbai India, 10.1145/2676726.2676964, https://figshare.com/articles/conference_contribution/From_Communicating_Machines_to_Graphical_Choreographies/10167236.
- Laura Bocchi;Hernán Melgratti;Emilio Tuosto, Lecture notes in computer science, Resolving Non-determinism in Choreographies, pp. 493-512, 2014, 10.1007/978-3-642-54833-8_26, https://doi.org/10.1007/978-3-642-54833-8_26.
- Laura Bocchi;Weizhen Yang;Nobuko Yoshida, Kent Academic Repository (University of Kent), Timed Multiparty Session Types, pp. 419-434, 2014, 10.1007/978-3-662-44584-6_29, https://kar.kent.ac.uk/43729/1/BYY14.pdf.
- Luca Fossati;Raymond Hu;Nobuko Yoshida, CiteSeer X (The Pennsylvania State University), Multiparty Session Nets, pp. 112-127, 2014, 10.1007/978-3-662-45917-1_8, http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.433.336.
- Luca Padovani, 2014, Fair subtyping for multi-party session types, 26, 3, pp. 424-464, 10.1017/s096012951400022x, https://hal.archives-ouvertes.fr/hal-00546531v2/document.
- Luca Padovani, Deadlock and lock freedom in the linear π-calculus, pp. 1-10, 2014, Vienna Austria, 10.1145/2603088.2603116, https://hal.inria.fr/hal-00932356.
- Mario Coppo;Mariangiola Dezani-Ciancaglini;Betti Venneri, Institutional Research Information System University of Turin (University of Turin), Self-Adaptive Monitors for Multiparty Sessions, pp. 688-696, 2014, Torino, Italy, 10.1109/pdp.2014.18, https://hdl.handle.net/2318/143611.
- Mario Coppo;Mariangiola Dezani-Ciancaglini;Betti Venneri, 2014, Self-adaptive multiparty sessions, Institutional Research Information System University of Turin (University of Turin), 9, 3-4, pp. 249-268, 10.1007/s11761-014-0171-9, http://hdl.handle.net/2318/154878.
- Mario Coppo;Mariangiola Dezani-Ciancaglini;Nobuko Yoshida;Luca Padovani, 2014, Global progress for dynamically interleaved multiparty sessions, Florence Research (University of Florence), 26, 2, pp. 238-302, 10.1017/s0960129514000188, https://hdl.handle.net/2158/1039582.
- Massimo Bartoletti;Alceste Scalas;Roberto Zunino, Lecture notes in computer science, A Semantic Deconstruction of Session Types, pp. 402-418, 2014, 10.1007/978-3-662-44584-6_28.
- Massimo Bartoletti;Julien Lange;Alceste Scalas;Roberto Zunino, 2014, Choreographies in the wild, Science of Computer Programming, 109, pp. 36-60, 10.1016/j.scico.2014.11.015, https://doi.org/10.1016/j.scico.2014.11.015.
- Nicholas Ng;Nobuko Yoshida, 2014 22nd Euromicro International Conference on Parallel, Distributed, and Network-Based Processing, Pabble: Parameterised Scribble for Parallel Programming, pp. 707-714, 2014, Torino, Italy, 10.1109/pdp.2014.20.
- Nicholas Ng;Nobuko Yoshida, 2014, Pabble: parameterised Scribble, Service Oriented Computing and Applications, 9, 3-4, pp. 269-284, 10.1007/s11761-014-0172-8, https://doi.org/10.1007/s11761-014-0172-8.
- Tzu-chun Chen, 2014, Lightening Global Types, arXiv (Cornell University), 155, pp. 38-46, 10.4204/eptcs.155.6.
- Davide Ancona;Matteo Barbieri;Viviana Mascardi, Proceedings of the 28th Annual ACM Symposium on Applied Computing, Constrained global types for dynamic checking of protocol conformance in multi-agent systems, 2013, Coimbra Portugal, 10.1145/2480362.2480620.
- Javier Esparza;Jörg Desel, arXiv (Cornell University), On Negotiation as Concurrency Primitive, pp. 440-454, 2013, 10.1007/978-3-642-40184-8_31, https://arxiv.org/abs/1307.2145.
- Julien Lange;Alceste Scalas, 2013, Choreography Synthesis as Contract Agreement, arXiv (Cornell University), 131, pp. 52-67, 10.4204/eptcs.131.6.
- Mila Dalla Preda;Maurizio Gabbrielli;Saverio Giallorenzo;Ivan Lanese;Jacopo Mauro, 2013, Developing correct, distributed, adaptive software, 97, pp. 41-46, 10.1016/j.scico.2013.11.019, https://hal.inria.fr/hal-01227610.
- Pierre-Malo Deniélou;Nobuko Yoshida, Spiral (Imperial College London), Multiparty Compatibility in Communicating Automata: Characterisation and Synthesis of Global Session Types, pp. 174-186, 2013, 10.1007/978-3-642-39212-2_18, http://hdl.handle.net/10044/1/95055.
- Zhenguo Yang;Farong Zhong;Jinfang Zhang, Lecture notes in computer science, A Polymorphic Type System with Progress for Binary Sessions, pp. 451-461, 2012, 10.1007/978-3-642-33469-6_57.
- Zhenguo Yang;Farong Zhong;Jinfang Zhang, 2012 13th International Conference on Parallel and Distributed Computing, Applications and Technologies, On Projections of Global Types in Partially Commutative Multiparty Asynchronous Sessions, pp. 563-568, 2012, Beijing, China, 10.1109/pdcat.2012.102.
Share and export
Consultation statistics
This page has been seen 2891 times.
This article's PDF has been downloaded 741 times.