, &{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.

M. Boreale and M. Bravetti, 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

D. Brand and P. Zafiropulo, On Communicating Finite-State Machines, Journal of the ACM, vol.30, issue.2, pp.323-342, 1983.
DOI : 10.1145/322374.322380

M. Bravetti, M. Carbone, and G. Zavattaro, 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

M. Bravetti, M. Carbone, and G. Zavattaro, 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

M. Bravetti and G. Zavattaro, 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

M. Bravetti and G. Zavattaro, 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

M. Bravetti and G. Zavattaro, 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

M. Bravetti and G. Zavattaro, A Foundational Theory of Contracts for Multi-party Service Composition, Fundamenta Informaticae, vol.89, issue.4, pp.451-478, 2008.

M. Bravetti and G. Zavattaro, 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

M. Bravetti and G. Zavattaro, 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

A. Brogi and J. Jacquet, 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

N. Busi, R. Gorrieri, and G. Zavattaro, 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

N. Busi, R. Gorrieri, and G. Zavattaro, 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

N. Busi, R. Gorrieri, and G. Zavattaro, 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

N. Busi and G. Zavattaro, 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

S. Carpineti, G. Castagna, C. Laneve, and L. Padovani, 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

N. Carriero and D. Gelernter, 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

G. Castagna, N. Gesbert, and L. Padovani, 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

T. Chen, M. Dezani-ciancaglini, A. Scalas, and N. Yoshida, 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

R. De-nicola, G. L. Ferrari, and R. Pugliese, 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

R. , D. Nicola, and R. Pugliese, 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

C. Dufourd, A. Finkel, and P. Schnoebelen, 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

A. Finkel and P. Schnoebelen, 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

C. Fournet, C. A. Hoare, S. K. Rajamani, and J. Rehof, 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

S. J. Gay and M. Hole, 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

D. Gelernter, 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

K. Honda, V. T. Vasconcelos, and M. Kubo, 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

K. Honda, N. Yoshida, and M. Carbone, 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

T. B. Jespersen, P. Munksgaard, and K. F. Larsen, Session types for rust, Proceedings of the 11th ACM SIGPLAN Workshop on Generic Programming, WGP 2015, pp.13-22, 2015.
DOI : 10.1017/S0956796809990268

D. Kozen, Automata and computability, 1997.
DOI : 10.1007/978-3-642-85706-5

C. Laneve and L. Padovani, 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

J. Lange and N. Yoshida, 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.

S. Lindley and J. G. Morris, 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

R. Milner, Communication and concurrency, 1989.

M. L. Minsky, Computation: finite and infinite machines, 1967.

D. Mostrous and N. Yoshida, 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

D. Mostrous, N. Yoshida, and K. Honda, 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

N. Ng and N. Yoshida, 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

A. Rensink and W. Vogler, Fair testing, Information and Computation, vol.205, issue.2, pp.125-198, 2007.
DOI : 10.1016/j.ic.2006.06.002

J. C. Shepherdson and H. E. Sturgis, Computability of Recursive Functions, Journal of the ACM, vol.10, issue.2, pp.217-255, 1963.
DOI : 10.1145/321160.321170