Observational Equivalence for Multiparty Sessions

• Autorzy: Severi Paula , Dezani-Ciancaglini Mariangiola

Identyfikatory

DOI

10.3233/FI-2019-1863

• Języki publikacji: EN

Abstrakty

EN

Multiparty sessions are concurrent processes, which allow several participants to communicate by sending and receiving messages. We consider an observational preorder of processes, that captures the idea that the whole session remains correct after replacing one process by another one. This preorder is characterised by means of a structural preorder between processes, which mimics the subtyping relation between session types from the literature.

Słowa kluczowe

EN

literature; multiparty session calculus; typing system

• Wydawca: Polskie Towarzystwo Matematyczne
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2019
• Tom: Vol. 170, nr 1-3
• Strony: 267--305
• Opis fizyczny: Bibliogr. 37 poz., rys., tab.

Twórcy

autor

Severi Paula

• Department of Computer Science, University of Leicester, Leicester, UK

autor

Dezani-Ciancaglini Mariangiola

• Dipartimento di Informatica, Università di Torino, Torino, Italy

Bibliografia

• [1] Honda K, Yoshida N, Carbone M. Multiparty Asynchronous Session Types. In: POPL. ACM Press, 2008 pp. 273-284. doi:10.1145/1328438.1328472.
• [2] Honda K, Yoshida N, Carbone M. Multiparty Asynchronous Session Types. Journal of the ACM, 2016. 63(1):9. doi:10.1145/2827695.
• [3] Coppo M, Dezani-Ciancaglini M, Yoshida N, Padovani L. Global Progress for Dynamically Interleaved Multiparty Sessions. Mathematical Structures in Computer Science, 2016. 26(2):238-302. doi:10.1017/S0960129514000188.
• [4] Gay S, Hole M. Subtyping for Session Types in the Pi-Calculus. Acta Informatica, 2005. 42(2/3):191-225. doi:10.1007/s00236-005-0177-z.
• [5] Demangeon R, Honda K. Full Abstraction in a Subtyped Pi-Calculus with Linear Types. In: CONCUR, volume 6901 of LNCS. Springer, 2011 pp. 280-296. doi:10.1007/978-3-642-23217-6_19.
• [6] Padovani L. Type Reconstruction for the Linear Pi-Calculus with Composite Regular Types. Logical Methods in Computer Science, 2015. 11(4). doi:10.2168/LMCS-11(4:13)2015.
• [7] Kobayashi N. A Type System for Lock-Free Processes. Information and Computation, 2002. 177(2):122-159. doi:10.1006/inco.2002.3171.
• [8] Dezani-Ciancaglini M, Ghilezan S, Jaksic S, Pantovic J, Yoshida N. Precise Subtyping for Synchronous Multiparty Sessions. In: PLACES, volume 203 of EPTCS. 2015 pp. 29-43. doi:10.4204/EPTCS.203.3.
• [9] Pierce BC. Types and Programming Languages. MIT Press, 2002. ISBN 978-0-262-16209-8.
• [10] Courcelle B. Fundamental Properties of Infinite Trees. Theoretical Computer Science, 1983. 25:95-169. doi:10.1016/0304-3975(83)90059-2.
• [11] Cardone F, Coppo M. Recursive Types. In: Barendregt H, Dekkers W, Statman R (eds.), Lambda Calculus with Types, Perspectives in Logic, pp. 377-576. Cambridge University Press. ISBN 978-0-521-76614-2, 2013.
• [12] Urzyczyn P. A Simple Proof of the Undecidability of Strong Normalisation. Mathematical Structures in Computer Science, 2003. 13(1):5-13. doi:10.1017/S096012950200381X.
• [13] Milner R. Communicating and Mobile Systems - the Pi-calculus. Cambridge University Press, 1999. ISBN 978-0-521-65869-0.
• [14] Deniélou P, Yoshida N. Dynamic Multirole Session Types. In: POPL. ACM Press, 2011 pp. 435-446. doi:10.1145/1926385.1926435.
• [15] Honda K. Types for Dyadic Interaction. In: CONCUR, volume 715 of LNCS. Springer, 1993 pp. 509-523. doi:10.1007/3-540-57208-2_35.
• [16] Honda K, Vasconcelos V, Kubo M. Language Primitives and Type Discipline for Structured Communication-Based Programming. In: ESOP, volume 1381 of LNCS. Springer, 1998 pp. 122-138. doi:10.1007/BFb0053567.
• [17] Bonelli E, Compagnoni A. Multipoint Session Types for a Distributed Calculus. In: TGC, volume 4912 of LNCS. Springer, 2007 pp. 240-256. doi:10.1007/978-3-540-78663-4_17.
• [18] Hüttel H, Lanese I, Vasconcelos V, Caires L, Carbone M, Deniélou P, Mostrous D, Padovani L, Ravara A, Tuosto E, Vieira H, Zavattaro G. Foundations of Session Types and Behavioural Contracts. ACM Computing Surveys, 2016. 49(1):3:1-3:36. doi:10.1145/2873052.
• [19] Padovani L. Session Types = Intersection Types + Union Types. In: ITRS, volume 45 of EPTCS. 2010 pp. 71-89. doi:10.4204/EPTCS.45.6.
• [20] Padovani L. On Projecting Processes into Session Types. Mathematical Structures in Computer Science, 2012. 22(2):237-289. doi:10.1017/S0960129511000405.
• [21] Barbanera F, de’Liguoro U. Sub-behaviour Relations for Session-based Client/Server Systems. Mathematical Structures in Computer Science, 2015. 25(6):1339-1381. doi:10.1017/S096012951400005X.
• [22] Bernardi G, Hennessy M. Modelling Session Types using Contracts. Mathematical Structures in Computer Science, 2016. 26(3):510-560. doi:10.1017/S0960129514000243.
• [23] Castagna G, Padovani L. Contracts for Mobile Processes. In: CONCUR, volume 5710 of LNCS. Springer, 2009 pp. 211-228. doi:10.1007/978-3-642-04081-8_15.
• [24] Kouzapas D, Yoshida N, Hu R, Honda K. On Asynchronous Eventful Session Semantics. Mathematical Structures in Computer Science, 2016. 26(2):303-364. doi:10.1017/S096012951400019X.
• [25] Kouzapas D, Pérez J, Yoshida N. Characteristic Bisimulation for Higher-order Session Processes. Acta Informatica, 2017. 54(3):271-341. doi:10.1007/s00236-016-0289-7.
• [26] Kouzapas D, Yoshida N. Globally Governed Session Semantics. Logical Methods in Computer Science, 2014. 10(4). doi:10.2168/LMCS-10(4:20)2014.
• [27] Urzyczyn P. Inhabitation in Typed Lambda-Calculi (A Syntactic Approach). In: TLCA, volume 1210 of LNCS. Springer, 1997 pp. 373-389. doi:10.1007/3-540-62688-3_47.
• [28] Urzyczyn P. Type Reconstruction in Fω. Mathematical Structures in Computer Science, 1997. 7(4):329-358. doi:10.1017/S0960129597002302.
• [29] Urzyczyn P. The Emptiness Problem for Intersection Types. Journal of Symbolic Logic, 1999. 64(3):1195-1215. doi:10.2307/2586625.
• [30] Urzyczyn P. Inhabitation of Low-Rank Intersection Types. In: TLCA, volume 5608 of LNCS. Springer, 2009 pp. 356-370. doi:10.1007/978-3-642-02273-9_26.
• [31] Rehof J, Urzyczyn P. The Complexity of Inhabitation with Explicit Intersection. In: Logic and Program Semantics, volume 7230 of LNCS. Springer, 2012 pp. 256-270. doi:10.1007/978-3-642-29485-3_16.
• [32] Ligatti J, Blackburn J, Nachtigal M. On Subtyping-Relation Completeness, with an Application to Iso-Recursive Types. ACM Transactions on Programming Languages and Systems, 2017. 39(1):4:1-4:36. doi:10.1145/2994596.
• [33] Gay S. Subtyping Supports Safe Session Substitution. In: A List of Successes That Can Change the World - Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday, volume 9600 of LNCS. Springer, 2016 pp. 95-108. doi:10.1007/978-3-319-30936-1_5.
• [34] Dezani-Ciancaglini M, Tiuryn J, Urzyczyn P. Discrimination by Parallel Observers: The Algorithm. Information and Computation, 1999. 150(2):153-186. doi:10.1006/inco.1998.2773.
• [35] Severi P, Padovani L, Tuosto E, Dezani-Ciancaglini M. On Sessions and Infinite Data. Logical Methods in Computer Science, 2017. 13(2). doi:10.23638/LMCS-13(2:9)2017.
• [36] Hu R, Yoshida N. Explicit Connection Actions in Multiparty Session Types. In: FASE, volume 10202 of LNCS. Springer, 2017 pp. 116-133. doi:10.1007/978-3-662-54494-5_7.
• [37] Brandt M, Henglein F. Coinductive Axiomatization of Recursive Type Equality and Subtyping. Fundamenta Informaticae, 1998. 33(4):309-338. doi:10.3233/FI-1998-33401.

Uwagi

Opracowanie rekordu w ramach umowy 509/P-DUN/2018 ze środków MNiSW przeznaczonych na działalność upowszechniającą naukę (2019).