,
, &{l i : T i } i?I ? reach(T ) implies T i ? reach(T ) for every i ? I; 3
, ?{l : T } ? reach(T ) implies T ? reach(T )
, Notice that reach(T ) contains the session types obtained by consuming initial inputs and outputs, and by unfolding recursion when it is at the top level
, Proposition 3 Given a single-out session type T , reach(T ) is finite and it is decidable whether antOutInf(T )
, Two notions of sub-behaviour for session-based client/server systems, Proc. of the 12th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, PPDP'10, pp.155-164, 2010.
, Advanced Mechanisms for Service Composition, Query and Discovery, Lecture Notes in Computer Science, vol.49, issue.2-3, pp.282-301, 2011.
DOI : 10.1016/0304-3975(87)90012-0
, On Communicating Finite-State Machines, Journal of the ACM, vol.30, issue.2, pp.323-342, 1983.
DOI : 10.1145/322374.322380
, Undecidability of asynchronous session subtyping, Information and Computation, vol.256, pp.300-320, 2017.
DOI : 10.1016/j.ic.2017.07.010
URL : https://hal.archives-ouvertes.fr/hal-01637935
, On the boundary between decidability and undecidability of asynchronous session subtyping, Theoretical Computer Science, vol.722, pp.19-51, 2018.
DOI : 10.1016/j.tcs.2018.02.010
URL : https://hal.archives-ouvertes.fr/hal-01921168
, Contract Based Multi-party Service Composition, Proc. of Int. Symposium on Fundamentals of Software Engineering, pp.207-222, 2007.
DOI : 10.1007/978-3-540-75698-9_14
, A Theory for Strong Service Compliance, Proc. of 9th Int. Conference on Coordination Models and Languages, pp.96-112, 2007.
DOI : 10.1007/978-3-540-72794-1_6
, Towards a Unifying Theory for Choreography Conformance and Contract Compliance, Proc. of 6th Int. Symposium Software Composition , SC'07, pp.34-50, 2007.
DOI : 10.1007/978-3-540-77351-1_4
, A Foundational Theory of Contracts for Multi-party Service Composition, Fundamenta Informaticae, vol.89, issue.4, pp.451-478, 2008.
, Contract Compliance and Choreography Conformance in the Presence of Message Queues, Proc. of 5th Int. Workshop on Web Services and Formal Methods, WS-FM'08, pp.37-54, 2008.
DOI : 10.1007/3-540-45657-0_13
, Choreographies and Behavioural Contracts on the Way to Dynamic Updates, Proc. 1st Workshop on Logics and Model-checking for Self-* Systems, pp.12-31, 2014.
DOI : 10.1016/j.ic.2006.06.002
URL : https://hal.archives-ouvertes.fr/hal-01090924
, Modeling coordination via asynchronous communication, Proc. of 2nd Int. Conference on Coordination Languages and Models, COORDI- NATION'97, pp.238-255, 1997.
DOI : 10.1007/3-540-63383-9_84
, On the Turing equivalence of Linda coordination primitives, Proc. of 4th Workshop on Expressiveness in Concurrency, EXPRESS'97, 1997.
DOI : 10.1016/S1571-0661(05)80467-0
URL : https://doi.org/10.1016/s1571-0661(05)80467-0
, Three semantics of the output operation for generative communication, Proc. of 2nd Int. Conference on Coordination Languages and Models, COORDINATION'97, pp.205-219, 1997.
DOI : 10.1007/3-540-63383-9_82
URL : http://www.cs.unibo.it/~zavattar/WWW/Publication/coord97.ps.gz
, Temporary Data in Shared Dataspace Coordination Languages, Proc. of 4th Int. Conference on Foundations of Software Science and Computation Structures, FOSSACS'01, pp.121-136, 2001.
DOI : 10.1007/3-540-45315-6_8
, On the Expressiveness of Event Notification in Data-Driven Coordination Languages, Proc. of 9th European Symposium on Programming, pp.41-55, 2000.
DOI : 10.1007/3-540-46425-5_3
, A Formal Account of Contracts for Web Services, Proc. of 3rd Int. Workshop on Web Services and Formal Methods, WS-FM'06, pp.148-162, 2006.
DOI : 10.1007/11841197_10
URL : https://hal.archives-ouvertes.fr/hal-00152568
, The s/net's linda kernel (extended abstract), Proc. of 10th ACM Symposium on Operating System Principles, pp.85-160, 1985.
DOI : 10.1145/323627.323643
, A theory of contracts for web services, Proc. of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL'08, pp.261-272, 2008.
DOI : 10.1145/1328897.1328471
URL : https://hal.archives-ouvertes.fr/hal-00277238
, On the Preciseness of Subtyping in Session Types, Proceedings of the 16th International Symposium on Principles and Practice of Declarative Programming, PPDP '14, p.2017
DOI : 10.1145/1599410.1599411
, Coordinating mobile agents via blackboards and access rights, Proc. of 2nd Int. Conference on Coordination Languages and Models, COORDINATION'97, pp.220-237, 1997.
DOI : 10.1007/3-540-63383-9_83
, A process algebra based on LINDA, Proc. of 1st Int. Conference on Coordination Languages and Models, COORDINATION'96, pp.160-178, 1996.
DOI : 10.1007/3-540-61052-9_45
, Reset nets between decidability and undecidability, Proc. of 25th Int. Colloquium on Automata, Languages and Programming , ICALP'98, pp.103-115, 1998.
DOI : 10.1007/BFb0055044
URL : http://www.lsv.ens-cachan.fr/Publis/PAPERS/DFS-icalp98.ps
, Well-structured transition systems everywhere! Theor, Comput. Sci, vol.256, issue.12, pp.63-92, 2001.
DOI : 10.1016/s0304-3975(00)00102-x
URL : https://doi.org/10.1016/s0304-3975(00)00102-x
, Stuck-Free Conformance, Proc. of 16th International Conference on Computer Aided Verification, pp.242-254, 2004.
DOI : 10.1007/978-3-540-27813-9_19
, Subtyping for session types in the pi calculus, Acta Informatica, vol.Analysis, issue.1, pp.191-225, 2005.
DOI : 10.1007/s00236-005-0177-z
, Generative communication in Linda, ACM Transactions on Programming Languages and Systems, vol.7, issue.1, pp.80-112, 1985.
DOI : 10.1145/2363.2433
URL : http://www.cis.umassd.edu/~hxu/courses/cis602/papers/p80-gelernter-linda.pdf
, Language primitives and type discipline for structured communication-based programming, Proc. of 7th European Symposium on Programming, ESOP'98, pp.122-138, 1998.
DOI : 10.1007/BFb0053567
URL : https://link.springer.com/content/pdf/10.1007%2FBFb0053567.pdf
, Multiparty asynchronous session types, Proc. of 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL'08, pp.273-284, 2008.
DOI : 10.1145/1328897.1328472
URL : http://www.doc.ic.ac.uk/~yoshida/multiparty/multiparty_full.pdf
, Session types for rust, Proceedings of the 11th ACM SIGPLAN Workshop on Generic Programming, WGP 2015, pp.13-22, 2015.
DOI : 10.1017/S0956796809990268
, Automata and computability, 1997.
DOI : 10.1007/978-3-642-85706-5
, The Must Preorder Revisited, Proc. of 18th Int. Conference Concurrency Theory, CONCUR'07, pp.212-225, 2007.
DOI : 10.1007/978-3-540-74407-8_15
, On the Undecidability of Asynchronous Session Subtyping
DOI : 10.1007/978-3-642-04167-9_12
, Proc. of 20th Int. Conference on Foundations of Software Science and Computation Structures, FOSSACS'17, pp.441-457, 2017.
, Embedding session types in Haskell, Proceedings of the 9th International Symposium on Haskell, Haskell 2016, pp.133-145, 2016.
DOI : 10.1017/S095679681400001X
URL : https://www.research.ed.ac.uk/portal/files/27373454/gvhs.pdf
, Communication and concurrency, 1989.
, Computation: finite and infinite machines, 1967.
, Session typing and asynchronous subtyping for the higher-order ??-calculus, Information and Computation, vol.241, pp.227-263, 2015.
DOI : 10.1016/j.ic.2015.02.002
URL : https://doi.org/10.1016/j.ic.2015.02.002
, Global Principal Typing in Partially Commutative Asynchronous Sessions, Proc. of 18th European Symposium on Programming, pp.316-332, 2009.
DOI : 10.1007/978-3-540-78739-6_21
URL : https://link.springer.com/content/pdf/10.1007%2F978-3-642-00590-9_23.pdf
, Static deadlock detection for concurrent go by global session graph synthesis, Proceedings of the 25th International Conference on Compiler Construction, CC 2016, pp.174-184, 2016.
DOI : 10.1007/3-540-58184-7_118
URL : http://spiral.imperial.ac.uk/bitstream/10044/1/34139/4/main.pdf
, OASIS. Web Services Business Process Execution Language Version 2.0 OASIS Standard
, Fair testing, Information and Computation, vol.205, issue.2, pp.125-198, 2007.
DOI : 10.1016/j.ic.2006.06.002
, Computability of Recursive Functions, Journal of the ACM, vol.10, issue.2, pp.217-255, 1963.
DOI : 10.1145/321160.321170