 |
 |
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
61 Documents citing this article
- Elaine Li;Felix Stutz;Thomas Wies, 2024, Deciding Subtyping for Asynchronous Multiparty Sessions, Lecture notes in computer science, pp. 176-205, 10.1007/978-3-031-57262-3_8, https://doi.org/10.1007/978-3-031-57262-3_8.
- Kirstin Peters;Nobuko Yoshida, 2024, Separation and Encodability in Mixed Choice Multiparty Sessions, Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science, pp. 1-15, 10.1145/3661814.3662085.
- Maurice H. ter Beek;Rolf Hennicker;José Proença, 2024, Team Automata: Overview and Roadmap, pp. 161-198, 10.1007/978-3-031-62697-5_10, https://inria.hal.science/hal-05009690.
- Elaine Li;Felix Stutz;Thomas Wies;Damien Zufferey, 2023, Complete Multiparty Session Type Projection with Automata, Lecture notes in computer science, pp. 350-373, 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, Electronic Proceedings in Theoretical Computer Science, 370, pp. 194-212, 10.4204/eptcs.370.13, https://doi.org/10.4204/eptcs.370.13.
- Ilaria Castellani;Mariangiola Dezani-Ciancaglini;Paola Giannini, 2022, Asynchronous Sessions with Input Races, Electronic Proceedings in Theoretical Computer Science, 356, pp. 12-23, 10.4204/eptcs.356.2, https://doi.org/10.4204/eptcs.356.2.
- Luc Edixhoven;Sung-Shik Jongmans, 2022, Realisability of Branching Pomsets, Lecture notes in computer science, pp. 185-204, 10.1007/978-3-031-20872-0_11.
- 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, IRIS UNIMORE (University of Modena and Reggio Emilia), 205, pp. 102610, 10.1016/j.scico.2021.102610, https://hdl.handle.net/11380/1331898.
- Davide Ancona;Angelo Ferrando;Viviana Mascardi, 2020, Can determinism and compositionality coexist in RML?, Electronic Proceedings in Theoretical Computer Science, 322, pp. 13-32, 10.4204/eptcs.322.4, https://doi.org/10.4204/eptcs.322.4.
- Ruben Hamers;Sung-Shik Jongmans, 2020, Discourje: Runtime Verification of Communication Protocols in Clojure, Lecture notes in computer science, pp. 266-284, 10.1007/978-3-030-45190-5_15, https://doi.org/10.1007/978-3-030-45190-5_15.
- Sung-Shik Jongmans;Nobuko Yoshida, 2020, Exploring Type-Level Bisimilarity towards More Expressive Multiparty Session Types, Lecture notes in computer science, pp. 251-279, 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.
- Maurizio Gabbrielli;Saverio Giallorenzo;Ivan Lanese;Jacopo Mauro, 2019, Guess Who’s Coming: Runtime Inclusion of Participants in Choreographies, Archivio istituzionale della ricerca (Alma Mater Studiorum Università di Bologna), pp. 118-138, 10.1007/978-3-030-31175-9_8, http://www.cs.unibo.it/projects/jolie/aiocj.html.
- Rolf Hennicker, 2019, Role-Based Development of Dynamically Evolving Esembles, pp. 3-24, 10.1007/978-3-030-23220-7_1, https://inria.hal.science/hal-02364578.
- Rolf Hennicker;Martin Wirsing, 2019, A Generic Dynamic Logic with Applications to Interaction-Based Systems, Lecture notes in computer science, pp. 172-187, 10.1007/978-3-030-30985-5_11.
- Angelo Ferrando, 2018, The early bird catches the worm: First verify, then monitor!, IRIS UNIMORE (University of Modena and Reggio Emilia), 172, pp. 160-179, 10.1016/j.scico.2018.11.008, https://hdl.handle.net/11380/1331882.
- Davide Ancona;Angelo Ferrando;Luca Franceschini;Viviana Mascardi, 2018, Coping with Bad Agent Interaction Protocols When Monitoring Partially Observable Multiagent Systems, IRIS UNIMORE (University of Modena and Reggio Emilia), pp. 59-71, 10.1007/978-3-319-94580-4_5, https://hdl.handle.net/11380/1331869.
- 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, Institutional Research Information System University of Turin (University of Turin), 100, pp. 16-35, 10.1016/j.jlamp.2018.06.001, http://hdl.handle.net/2318/1670197.
- Rolf Hennicker;Martin Wirsing, 2018, Dynamic Logic for Ensembles, Lecture notes in computer science, pp. 32-47, 10.1007/978-3-030-03424-5_3.
- Emilio Tuosto;Roberto Guanciale, 2017, Semantics of global view of choreographies, Leicester Research Archive (University of Leicester), 95, pp. 17-40, 10.1016/j.jlamp.2017.11.002, http://www.sciencedirect.com/science/article/pii/S2352220816301754?via%3Dihub.
- Ilaria Castellani;Mariangiola Dezani-Ciancaglini;Paola Giannini, 2017, Concurrent Reversible Sessions, Leibniz-Zentrum für Informatik (Schloss Dagstuhl), 10.4230/lipics.concur.2017.30, https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2017.30.
- Davide Ancona;Angelo Ferrando;Viviana Mascardi, 2016, Comparing Trace Expressions and Linear Temporal Logic for Runtime Verification, IRIS UNIMORE (University of Modena and Reggio Emilia), pp. 47-64, 10.1007/978-3-319-30734-3_6, https://hdl.handle.net/11380/1331905.
- 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, 2016, Enforcing Availability in Failure-Aware Communicating Systems, pp. 195-211, 10.1007/978-3-319-39570-8_13, https://inria.hal.science/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, Electronic Proceedings in Theoretical Computer Science, 223, pp. 67-82, 10.4204/eptcs.223.5, https://doi.org/10.4204/eptcs.223.5.
- Alberto Lluch Lafuente;Flemming Nielson;Hanne Riis Nielson, 2015, Discretionary Information Flow Control for Interaction-Oriented Specifications, Research Portal (King's College London), pp. 427-450, 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, IRIS UNIMORE (University of Modena and Reggio Emilia), 9, 2, pp. 131-148, 10.3233/ia-150084, https://hdl.handle.net/11380/1331886.
- Ivan Lanese;Fabrizio Montesi;Gianluigi Zavattaro, 2015, The Evolution of Jolie, pp. 506-521, 10.1007/978-3-319-15545-6_29, https://inria.hal.science/hal-01227623.
- Julien Lange;Emilio Tuosto;Nobuko Yoshida, 2015, From Communicating Machines to Graphical Choreographies, ACM SIGPLAN Notices, 50, 1, pp. 221-232, 10.1145/2775051.2676964.
- Mario Coppo;Mariangiola Dezani-Ciancaglini;Luca Padovani;Nobuko Yoshida, 2015, A Gentle Introduction to Multiparty Asynchronous Session Types, Lecture notes in computer science, pp. 146-178, 10.1007/978-3-319-18941-3_4.
- 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.
- Mila Dalla Preda;Maurizio Gabbrielli;Saverio Giallorenzo;Ivan Lanese;Jacopo Mauro, 2015, Dynamic Choreographies, pp. 67-82, 10.1007/978-3-319-19282-6_5, https://inria.hal.science/hal-01227612.
- 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.
- Davide Ancona;Daniela Briola;Amal El Fallah Seghrouchni;Viviana Mascardi;Patrick Taillibert, 2014, Efficient Verification of MASs with Projections, Lecture notes in computer science, pp. 246-270, 10.1007/978-3-319-14484-9_13.
- Davide Basile;Pierpaolo Degano;Gian Luigi Ferrari, 2014, Automata for Analysing Service Contracts, Lecture notes in computer science, pp. 34-50, 10.1007/978-3-662-45917-1_3.
- Julien Lange;Emilio Tuosto;Nobuko Yoshida, 2014, From Communicating Machines to Graphical Choreographies, Leicester Research Archive (University of Leicester), pp. 221-232, 10.1145/2676726.2676964, http://dl.acm.org/citation.cfm?doid=2676726.2676964.
- LUCA PADOVANI, 2014, Fair subtyping for multi-party session types, Mathematical Structures in Computer Science, 26, 3, pp. 424-464, 10.1017/s096012951400022x, https://doi.org/10.1017/s096012951400022x.
- Laura Bocchi;Hernán Melgratti;Emilio Tuosto, 2014, Resolving Non-determinism in Choreographies, Lecture notes in computer science, pp. 493-512, 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, 2014, Timed Multiparty Session Types, Spiral (Imperial College London), pp. 419-434, 10.1007/978-3-662-44584-6_29, http://hdl.handle.net/10044/1/95030.
- Luca Fossati;Raymond Hu;Nobuko Yoshida, 2014, Multiparty Session Nets, Lecture notes in computer science, pp. 112-127, 10.1007/978-3-662-45917-1_8.
- Luca Padovani, 2014, Deadlock and lock freedom in the linear π-calculus, Institutional Research Information System University of Turin (University of Turin), pp. 1-10, 10.1145/2603088.2603116, http://hdl.handle.net/2318/153607.
- MARIO COPPO;MARIANGIOLA DEZANI-CIANCAGLINI;NOBUKO YOSHIDA;LUCA PADOVANI, 2014, Global progress for dynamically interleaved multiparty sessions, Institutional Research Information System University of Turin (University of Turin), 26, 2, pp. 238-302, 10.1017/s0960129514000188, http://hdl.handle.net/2318/154508.
- 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;Betti Venneri, 2014, Self-Adaptive Monitors for Multiparty Sessions, Florence Research (University of Florence), pp. 688-696, 10.1109/pdp.2014.18.
- Massimo Bartoletti;Alceste Scalas;Roberto Zunino, 2014, A Semantic Deconstruction of Session Types, Lecture notes in computer science, pp. 402-418, 10.1007/978-3-662-44584-6_28.
- Massimo Bartoletti;Julien Lange;Alceste Scalas;Roberto Zunino, 2014, Choreographies in the wild, Aston Publications Explorer (Aston University), 109, pp. 36-60, 10.1016/j.scico.2014.11.015, https://publications.aston.ac.uk/view/author/8284d2a758b4deb7bfc43572bf956ce8.html>.
- Nicholas Ng;Nobuko Yoshida, 2014, Pabble: Parameterised Scribble for Parallel Programming, 2014 22nd Euromicro International Conference on Parallel, Distributed, and Network-Based Processing, 5502, pp. 707-714, 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, Electronic Proceedings in Theoretical Computer Science, 155, pp. 38-46, 10.4204/eptcs.155.6, https://doi.org/10.4204/eptcs.155.6.
- Davide Ancona;Matteo Barbieri;Viviana Mascardi, 2013, Constrained global types for dynamic checking of protocol conformance in multi-agent systems, CINECA IRIS Institutial Research Information System (University of Genoa), pp. 1377-1379, 10.1145/2480362.2480620.
- Javier Esparza;Jörg Desel, 2013, On Negotiation as Concurrency Primitive, Lecture notes in computer science, pp. 440-454, 10.1007/978-3-642-40184-8_31.
- Julien Lange;Alceste Scalas, 2013, Choreography Synthesis as Contract Agreement, Electronic Proceedings in Theoretical Computer Science, 131, pp. 52-67, 10.4204/eptcs.131.6, https://doi.org/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://inria.hal.science/hal-01227610.
- Pierre-Malo Deniélou;Nobuko Yoshida, 2013, Multiparty Compatibility in Communicating Automata: Characterisation and Synthesis of Global Session Types, Spiral (Imperial College London), pp. 174-186, 10.1007/978-3-642-39212-2_18, http://hdl.handle.net/10044/1/95055.
- Zhenguo Yang;Farong Zhong;Jinfang Zhang, 2012, On Projections of Global Types in Partially Commutative Multiparty Asynchronous Sessions, 2012 13th International Conference on Parallel and Distributed Computing, Applications and Technologies, 5502, pp. 563-568, 10.1109/pdcat.2012.102.
- Zhenguo Yang;Farong Zhong;Jinfang Zhang, 2012, A Polymorphic Type System with Progress for Binary Sessions, Lecture notes in computer science, pp. 451-461, 10.1007/978-3-642-33469-6_57.
Share and export
Consultation statistics
This page has been seen 4877 times.
This article's PDF has been downloaded 1038 times.