HORNE, Ross James ; University of Luxembourg > Faculty of Science, Technology and Communication (FSTC) > Computer Science and Communications Research Unit (CSC)
External co-authors :
no
Language :
English
Title :
Session Subtyping and Multiparty Compatibility Using Circular Sequents
Publication date :
2020
Event name :
In 31st International Conference on Concurrency Theory (CONCUR 2020).
Event date :
1-4 September 2020
Main work title :
In 31st International Conference on Concurrency Theory (CONCUR 2020).
Samson Abramsky. Computational interpretations of linear logic. Theoretical computer science, 111(1):3-57, 1993. doi:10.1016/0304-3975(93)90181-R.
Roberto M. Amadio and Luca Cardelli. Subtyping recursive types. ACM Trans. Program. Lang. Syst., 15(4):575-631, September 1993. doi:10.1145/155183.155231.
Jean-Marc Andreoli. Logic programming with focusing proofs in linear logic. Journal of Logic and Computation, 2(3):297-347, 1992. doi:10.1093/logcom/2.3.297.
David Baelde, Amina Doumane, and Alexis Saurin. Infinitary Proof Theory: the Multiplicative Additive Case. In Jean-Marc Talbot and Laurent Regnier, editors, 25th EACSL Annual Conference on Computer Science Logic (CSL 2016), volume 62 of LIPIcs, pages 42:1-42:17. Schloss Dagstuhl, 2016. doi:10.4230/LIPIcs.CSL.2016.42.
Franco Barbanera and Ugo de'Liguoro. Sub-behaviour relations for session-based client/server systems. Mathematical Structures in Computer Science, 25(6):1339-1381, 2015. doi:10.1017/ S096012951400005X.
Franco Barbanera and Mariangiola Dezani-Ciancaglini. Open multiparty sessions. In Proceedings 12th Interaction and Concurrency Experience, ICE 2019, Copenhagen, Denmark, 20-21 June 2019., pages 77-96, 2019. doi:10.4204/EPTCS.304.6.
Giovanni Bernardi and Matthew Hennessy. Using higher-order contracts to model session types. Logical Methods in Computer Science, 12(2), 2016. doi:10.2168/LMCS-12(2:10)2016.
Eduardo Bonelli and Adriana Compagnoni. Multipoint session types for a distributed calculus. In Gilles Barthe and Cédric Fournet, editors, Trustworthy Global Computing, pages 240-256. Springer, 2008. doi:10.1007/978-3-540-78663-4_17.
James Brotherston and Alex Simpson. Sequent calculi for induction and infinite descent. Journal of Logic and Computation, 21(6):1177-1216, October 2010. doi:10.1093/logcom/ exq052.
Paola Bruscoli. A purely logical account of sequentiality in proof search. In Peter J. Stuckey, editor, Logic Programming, pages 302-316. Springer, 2002. doi:10.1007/3-540-45619-8_21.
Luís Caires and Jorge A. Pérez. Multiparty session types within a canonical binary theory, and beyond. In FORTE 2016, pages 74-95, 2016. doi:10.1007/978-3-319-39570-8_6.
Marco Carbone, Fabrizio Montesi, Carsten Schürmann, and Nobuko Yoshida. Multiparty session types as coherence proofs. Acta Informatica, 54(3):243-269, 2017. doi:10.1007/ s00236-016-0285-y.
Ilaria Castellani, Mariangiola Dezani-Ciancaglini, Paola Giannini, and Ross Horne. Global types with internal delegation. Theoretical Computer Science, 807:128-153, 2020. doi: 10.1016/j.tcs.2019.09.027.
Tzu-chun Chen, Mariangiola Dezani-Ciancaglini, Alceste Scalas, and Nobuko Yoshida. On the Preciseness of Subtyping in Session Types. Logical Methods in Computer Science, Volume 13, Issue 2, 2017. doi:10.23638/LMCS-13(2:12)2017.
Gabriel Ciobanu and Ross Horne. Behavioural analysis of sessions using the calculus of structures. In Perspectives of System Informatics - 10th International Andrei Ershov Informatics Conference, PSI 2015, pages 91-106, 2015. doi:10.1007/978-3-319-41579-6_8.
Ugo Dal Lago, Marc de Visme, Damiano Mazza, and Akira Yoshimizu. Intersection types and runtime errors in the pi-calculus. Proc. ACM Program. Lang., 3(POPL), 2019. doi: 10.1145/3290320.
Rocco De Nicola and Matthew Hennessy. CCS without τ's. In Hartmut Ehrig, Robert Kowalski, Giorgio Levi, and Ugo Montanari, editors, TAPSOFT'87, pages 138-152. Springer, 1987. doi:10.1007/3-540-17660-8_53.
Romain Demangeon and Kohei Honda. Full abstraction in a subtyped pi-calculus with linear types. In CONCUR, volume 6901 of LNCS, pages 280-296. Springer, 2011. doi: 10.1007/978-3-642-23217-6_19.
Pierre-Malo Deniélou and Nobuko Yoshida. Multiparty session types meet communicating automata. In Helmut Seidl, editor, Programming Languages and Systems, pages 194-213. Springer, 2012. doi:10.1007/978-3-642-28869-2_10.
Pierre-Malo Deniélou and Nobuko Yoshida. Multiparty compatibility in communicating automata: Characterisation and synthesis of global session types. In Automata, Languages, and Programming, pages 174-186. Springer, 2013. doi:10.1007/978-3-642-39212-2_18.
Pierre-Malo Deniélou, Nobuko Yoshida, Andi Bejleri, and Raymond Hu. Parameterised multiparty session types. Logical Methods in Computer Science, 8(4), 2012. doi:10.2168/ LMCS-8(4:6)2012.
Farzaneh Derakhshan and Frank Pfenning. Circular proof as session-typed processes: a local validity condition. CoRR, 2019. arXiv:1908.01909.
Simon Gay and Malcolm Hole. Subtyping for session types in the pi calculus. Acta Informatica, 42(2-3):191-225, 2005. doi:10.1007/s00236-005-0177-z.
Simon J. Gay and Malcolm Hole. Types and subtypes for client-server interactions. In ESOP, volume 1576 of Lecture Notes in Computer Science, pages 74-90. Springer, 1999. doi:10.1007/3-540-49099-X_6.
Silvia Ghilezan, Svetlana Jaksic, Jovanka Pantovic, Alceste Scalas, and Nobuko Yoshida. Precise subtyping for synchronous multiparty sessions. J. Log. Algebr. Meth. Program., 104:127-173, 2019. doi:10.1016/j.jlamp.2018.12.002.
Jean-Yves Girard and Yves Lafont. Linear logic and lazy computation. In Hartmut Ehrig, Robert Kowalski, Giorgio Levi, and Ugo Montanari, editors, TAPSOFT'87, pages 52-66. Springer, 1987. doi:10.1007/BFb0014972.
Alessio Guglielmi. A system of interaction and structure. ACM Transactions on Compututational Logic, 8, 2007. doi:10.1145/1182613.1182614.
Dick Hardt. The OAuth 2.0 authorization framework. standard rfc6749, Internet Engineering Task Force, 2012. URL: https://tools.ietf.org/html/rfc6749.
Kohei Honda. Types for dyadic interaction. In CONCUR'93, pages 509-523. Springer, 1993. doi:10.1007/3-540-57208-2_35.
Kohei Honda, Aybek Mukhamedov, Gary Brown, Tzu-Chun Chen, and Nobuko Yoshida. Scribbling interactions with a formal foundation. In Raja Natarajan and Adegboyega Ojo, editors, Distributed Computing and Internet Technology, pages 55-75. Springer, 2011. doi: 10.1007/978-3-642-19056-8_4.
Kohei Honda, Nobuko Yoshida, and Marco Carbone. Multiparty asynchronous session types. In Proceedings of the 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL'08, pages 273-284. ACM, 2008. doi:10.1145/1328438. 1328472.
Kohei Honda, Nobuko Yoshida, and Marco Carbone. Multiparty asynchronous session types. J. ACM, 63(1):9:1-9:67, 2016. doi:10.1145/2827695.
Ross Horne. The consistency and complexity of multiplicative additive system virtual. Scientific Annals of Computer Science, 25(2):245-316, 2015. doi:10.7561/SACS.2015.2.245.
Ross Horne. The sub-additives: A proof theory for probabilistic choice extending linear logic. In 4th International Conference on Formal Structures for Computation and Deduction, FSCD 2019, pages 23:1-23:16, 2019. doi:10.4230/LIPIcs.FSCD.2019.23.
Ross Horne and Alwen Tiu. Constructing weak simulations from linear implications for processes with private names. Mathematical Structures in Computer Science, 29(8):1275-1308, 2019. doi:10.1017/S0960129518000452.
Naoki Kobayashi. A type system for lock-free processes. Information and Computation, 177(2):122-159, 2002. doi:10.1016/S0890-5401(02)93171-8.
Julien Lange and Emilio Tuosto. Synthesising choreographies from local session types. In Maciej Koutny and Irek Ulidowski, editors, CONCUR 2012 - Concurrency Theory, pages 225-239. Springer, 2012.
Julien Lange, Emilio Tuosto, and Nobuko Yoshida. From communicating machines to graphical choreographies. In Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL'15, pages 221-232. ACM, 2015. doi: 10.1145/2676726.2676964.
Sam Lindley and J. Garrett Morris. Talking bananas: Structural recursion for session types. In Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, ICFP 2016, page 434-447. ACM, 2016. doi:10.1145/2951913.2951921.
Barbara Liskov and Jeannette M. Wing. A behavioral notion of subtyping. ACM Trans. Program. Lang. Syst., 16(6):1811-1841, 1994. doi:10.1145/197320.197383.
Dale Miller, Gopalan Nadathur, Frank Pfenning, and Andre Scedrov. Uniform proofs as a foundation for logic programming. Annals of Pure and Applied Logic, 51(1):125-157, 1991. doi:10.1016/0168-0072(91)90068-W.
Dimitris Mostrous, Nobuko Yoshida, and Kohei Honda. Global principal typing in partially commutative asynchronous sessions. In Programming Languages and Systems, pages 316-332. Springer, 2009. doi:10.1007/978-3-642-00590-9_23.
Luca Padovani. Session types = intersection types + union types. In Proceedings Fifth Workshop on Intersection Types and Related Systems, ITRS 2010, Edinburgh, U.K., 9th July 2010., pages 71-89, 2010. doi:10.4204/EPTCS.45.6.
Luca Padovani. On projecting processes into session types. Mathematical Structures in Computer Science, 22(2):237-289, 2012. doi:10.1017/S0960129511000405.
Luca Padovani. Deadlock and lock freedom in the linear pi-calculus. In CSL-LICS, pages 72:1-72:10. ACM Press, 2014. doi:10.1145/2603088.2603116.
Benjamin C. Pierce and Davide Sangiorgi. Typing and subtyping for mobile processes. Mathematical Structures in Computer Science, 6(5):409-453, 1996. doi:10.1017/S096012950007002X.
Alceste Scalas and Nobuko Yoshida. Less is more: multiparty session types revisited. PACMPL, 3(POPL):30:1-30:29, 2019. doi:10.1145/3290343.
Paula Severi and Mariangiola Dezani-Ciancaglini. Observational equivalence for multiparty sessions. Fundam. Inform., 170(1-3):267-305, 2019. doi:10.3233/FI-2019-1863.
Alwen Tiu. A system of interaction and structure II: The need for deep inference. Logical Methods in Computer Science, 2(2), 2006. doi:10.2168/LMCS-2(2:4)2006.
