M. Abadi, L. Cardelli, B. Pierce, and G. Plotkin, Dynamic typing in a statically typed language, ACM Transactions on Programming Languages and Systems, vol.13, issue.2, pp.237-268, 1991.
DOI : 10.1145/103135.103138

D. Ancona, V. Bono, M. Bravetti, G. Castagna, J. Campos et al., Behavioral Types in Programming Languages, Foundations and Trends?? in Programming Languages, vol.3, issue.2-3, 2014.
DOI : 10.1561/2500000031

URL : https://hal.archives-ouvertes.fr/hal-01348054

P. Baltazar, L. Caires, V. T. Vasconcelos, and H. T. Vieira, A Type System for Flexible Role Assignment in Multiparty Communicating Systems, TGC 2012, pp.82-96, 2013.
DOI : 10.1007/978-3-642-41157-1_6

P. Baltazar, D. Mostrous, and V. T. Vasconcelos, Linearly Refined Session Types, LINEARITY 2012, pp.38-49, 2012.
DOI : 10.4204/EPTCS.101.4

URL : http://doi.org/10.4204/eptcs.101.4

F. Barbanera and U. De-'liguoro, Two notions of sub-behaviour for session-based client/server systems, Proceedings of the 12th international ACM SIGPLAN symposium on Principles and practice of declarative programming, PPDP '10, pp.155-164, 2010.
DOI : 10.1145/1836089.1836109

J. Barnes, High Integrity Software: The SPARK Approach to Safety and Security, 2003.

M. Bartoletti, T. Cimoli, G. M. Pinna, and R. Zunino, Contracts as games on event structures, Journal of Logical and Algebraic Methods in Programming, vol.85, issue.3, 2015.
DOI : 10.1016/j.jlamp.2015.05.001

M. Bartoletti, T. Cimoli, and R. Zunino, A Theory of Agreements and Protection, POST 2013, pp.186-205, 2013.
DOI : 10.1007/978-3-642-36830-1_10

M. Bartoletti, M. Murgia, A. Scalas, and R. Zunino, Modelling and Verifying Contract-Oriented Systems in Maude, WRLA 2014, pp.130-146, 2014.
DOI : 10.1007/978-3-319-12904-4_7

M. Bartoletti, A. Scalas, E. Tuosto, and R. Zunino, Honesty by Typing, FMOODS/FORTE 2013, pp.305-320, 2013.
DOI : 10.1007/978-3-642-38592-6_21

M. Bartoletti, E. Tuosto, and R. Zunino, On the Realizability of Contracts in Dishonest Systems, COORDINATION 2012, pp.245-260, 2012.
DOI : 10.1007/978-3-642-30829-1_17

L. Bettini, M. Coppo, L. D. Antoni, M. D. Luca, M. Dezani-ciancaglini et al., Global Progress in Dynamically Interleaved Multiparty Sessions, LNCS, vol.5201, pp.418-433, 2008.
DOI : 10.1007/978-3-540-85361-9_33

K. Bhargavan, R. Corin, P. Deniélou, C. Fournet, and J. J. Leifer, Cryptographic Protocol Synthesis and Verification for Multiparty Sessions, 2009 22nd IEEE Computer Security Foundations Symposium, pp.124-140, 2009.
DOI : 10.1109/CSF.2009.26

L. Bocchi, T. Chen, R. Demangeon, K. Honda, and N. Yoshida, Monitoring networks through multiparty session types, FMOODS/FORTE 2013, pp.50-65, 2013.
URL : https://hal.archives-ouvertes.fr/hal-01213683

L. Bocchi, K. Honda, E. Tuosto, and N. Yoshida, A Theory of Design-by-Contract for Distributed Multiparty Interactions, CONCUR 2010, pp.162-176, 2010.
DOI : 10.1007/978-3-642-15375-4_12

E. Bonelli, A. B. Compagnoni, and E. L. Gunter, Correspondence assertions for process synchronization in concurrent communications, Journal of Functional Programming, vol.15, issue.2, pp.219-247, 2005.
DOI : 10.1017/S095679680400543X

M. Boreale, R. Bruni, L. Caires, R. De-nicola, I. Lanese et al., SCC: A Service Centered Calculus, WS-FM 2006, pp.38-57, 2006.
DOI : 10.1007/11841197_3

A. Bossi, R. Focardi, C. Piazza, and S. Rossi, Verifying persistent security properties, Computer Languages, Systems & Structures, vol.30, issue.3-4, pp.3-4231, 2004.
DOI : 10.1016/j.cl.2004.02.005

R. Bruni and L. G. Mezzina, Types and Deadlock Freedom in a Calculus of Services, Sessions and Pipelines, AMAST 2008, pp.100-115, 2008.
DOI : 10.1007/978-3-540-79980-1_8

L. Caires and F. Pfenning, Session Types as Intuitionistic Linear Propositions, CONCUR 2010, pp.222-236, 2010.
DOI : 10.1007/978-3-642-15375-4_16

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=

S. Capecchi, I. Castellani, and M. Dezani-ciancaglini, Typing access control and secure information flow in sessions, Information and Computation, vol.238, pp.68-105, 2014.
DOI : 10.1016/j.ic.2014.07.005

URL : https://hal.archives-ouvertes.fr/hal-01088782

S. Capecchi, I. Castellani, and M. Dezani-ciancaglini, Information flow safety in multiparty sessions, Math. Struct. in Comp. Science, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01237236

S. Capecchi, I. Castellani, M. Dezani-ciancaglini, and T. Rezk, Session Types for Access and Information Flow Control, CONCUR 2010, pp.237-252, 2010.
DOI : 10.1007/978-3-642-15375-4_17

URL : https://hal.archives-ouvertes.fr/inria-00511304

I. Castellani, M. Dezani-ciancaglini, and J. A. Pérez, Self-Adaptation and Secure Information Flow in Multiparty Structured Communications: A Unified Perspective, BEAT 2014, pp.9-18, 2014.
DOI : 10.4204/EPTCS.162.2

URL : https://hal.archives-ouvertes.fr/hal-01088437

T. Chen, L. Bocchi, P. Deniélou, K. Honda, and N. Yoshida, Asynchronous Distributed Monitoring for Multiparty Session Enforcement, TGC 2011, pp.25-45, 2012.
DOI : 10.1007/978-3-642-30065-3_2

S. Chong, A. C. Myers, K. Vikram, and L. Zheng, Jif Reference Manual, 2009.

R. Corin and P. Deniélou, A Protocol Compiler for Secure Sessions in ML, TGC 2007, pp.276-293, 2007.
DOI : 10.1007/978-3-540-78663-4_19

R. Corin, P. Deniélou, C. Fournet, K. Bhargavan, and J. J. Leifer, Secure Implementations for Typed Session Abstractions, 20th IEEE Computer Security Foundations Symposium (CSF'07), pp.170-186, 2007.
DOI : 10.1109/CSF.2007.29

R. Corin, P. Deniélou, C. Fournet, K. Bhargavan, and J. J. Leifer, A secure compiler for session abstractions, Journal of Computer Security, vol.16, issue.5, pp.573-636, 2008.
DOI : 10.3233/JCS-2008-0334

S. Crafa and S. Rossi, A theory of noninterference for the pi-calculus, TGC 2005, pp.2-18, 2005.

P. Deniélou and N. Yoshida, Multiparty Session Types Meet Communicating Automata, ESOP 2012, pp.194-213, 2012.
DOI : 10.1007/978-3-642-28869-2_10

D. E. Denning and P. J. Denning, Certification of programs for secure information flow, Communications of the ACM, vol.20, issue.7, pp.504-513, 1977.
DOI : 10.1145/359636.359712

M. Dezani-ciancaglini, S. Drossopoulou, D. Mostrous, and N. Yoshida, Objects and session types, Information and Computation, vol.207, issue.5, pp.595-641, 2009.
DOI : 10.1016/j.ic.2008.03.028

URL : https://hal.archives-ouvertes.fr/hal-00909312

M. Dezani-ciancaglini, S. Ghilezan, S. Jaksic, and J. Pantovic, Types for rolebased access control of dynamic web data, WFLP 2010, pp.1-29, 2010.

M. Dezani-ciancaglini, S. Ghilezan, and J. Pantovic, Security types for dynamic web data, TGC 2006, pp.263-280, 2006.
URL : https://hal.archives-ouvertes.fr/hal-00149049

M. Dezani-ciancaglini, S. Ghilezan, J. Pantovic, and D. Varacca, Security types for dynamic web data, Theoretical Computer Science, vol.402, issue.2-3, pp.156-171, 2008.
DOI : 10.1016/j.tcs.2008.04.032

URL : https://hal.archives-ouvertes.fr/hal-00149049

T. Disney and C. Flanagan, Gradual information flow typing, 2011.

M. Fähndrich, M. Aiken, C. Hawblitzel, O. Hodson, G. C. Hunt et al., Language support for fast and reliable message-based communication in singularity OS, EuroSys, pp.177-190, 2006.

L. Fennell and P. Thiemann, The Blame Theorem for a Linear Lambda Calculus with Type Dynamic, TFP 2012, pp.37-52, 2012.
DOI : 10.1007/978-3-642-40447-4_3

L. Fennell and P. Thiemann, Gradual Security Typing with References, 2013 IEEE 26th Computer Security Foundations Symposium, pp.224-239, 2013.
DOI : 10.1109/CSF.2013.22

L. Fennell and P. Thiemann, Gradual typing for annotated type systems, ESOP 2014, pp.47-66, 2014.

R. Focardi and R. Gorrieri, Foundations of Security Analysis and Design, Tutorial Lectures, LNCS, vol.2171, 2001.

P. Gardner and S. Maffeis, Modelling dynamic web data, Theoretical Computer Science, vol.342, issue.1, pp.104-131, 2005.
DOI : 10.1016/j.tcs.2005.06.006

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=

D. Garg and F. Pfenning, A Proof-Carrying File System, 2010 IEEE Symposium on Security and Privacy, pp.349-364, 2010.
DOI : 10.1109/SP.2010.28

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

S. Ghilezan, S. Jaksic, J. Pantovic, and M. Dezani-ciancaglini, Types and roles for web security, Trans. Adv. Res, vol.8, issue.2, pp.16-21, 2012.

S. Ghilezan, S. Jaksic, J. Pantovic, J. A. Pérez, and H. T. Vieira, Dynamic Role Authorization in Multiparty Conversations, BEAT 2014, pp.1-8, 2014.
DOI : 10.4204/EPTCS.162.1

J. Girard, Linear logic, Theoretical Computer Science, vol.50, issue.1, pp.1-102, 1987.
DOI : 10.1016/0304-3975(87)90045-4

URL : https://hal.archives-ouvertes.fr/inria-00075966

J. A. Goguen and J. Meseguer, Security Policies and Security Models, 1982 IEEE Symposium on Security and Privacy, pp.11-20, 1982.
DOI : 10.1109/SP.1982.10014

A. D. Gordon and A. Jeffrey, Typing correspondence assertions for communication protocols, Theoretical Computer Science, vol.300, issue.1-3, pp.379-409, 2003.
DOI : 10.1016/S0304-3975(02)00333-X

R. Harper, F. Honsell, and G. Plotkin, A framework for defining logics, Journal of the ACM, vol.40, issue.1, pp.143-184, 1993.
DOI : 10.1145/138027.138060

D. Hedin, A. Birgisson, L. Bello, and A. Sabelfeld, JSFlow, Proceedings of the 29th Annual ACM Symposium on Applied Computing, SAC '14, pp.1663-1671, 2014.
DOI : 10.1145/2554850.2554909

F. Henglein, Dynamic typing: syntax and proof theory, Science of Computer Programming, vol.22, issue.3, pp.197-230, 1994.
DOI : 10.1016/0167-6423(94)00004-2

URL : http://doi.org/10.1016/0167-6423(94)00004-2

M. Hennessy, The security pi-calculus and non-interference, The Journal of Logic and Algebraic Programming, vol.63, issue.1, pp.3-34, 2005.
DOI : 10.1016/j.jlap.2004.01.003

M. Hennessy and J. Riely, Information flow vs. resource access in the asynchronous pi-calculus, ACM Transactions on Programming Languages and Systems, vol.24, issue.5, pp.566-591, 2002.
DOI : 10.1145/570886.570890

K. Honda, Types for dyadic interaction, LNCS, vol.715, pp.509-523, 1993.
DOI : 10.1007/3-540-57208-2_35

K. Honda, V. T. Vasconcelos, and M. Kubo, Language primitives and type discipline for structured communication-based programming, LNCS, vol.1381, pp.122-138, 1998.
DOI : 10.1007/BFb0053567

K. Honda, V. T. Vasconcelos, and N. Yoshida, Secure Information Flow as Typed Process Behaviour, LNCS, vol.1782, pp.180-199, 2000.
DOI : 10.1007/3-540-46425-5_12

K. Honda and N. Yoshida, A uniform type structure for secure information flow, ACM Trans. Program. Lang. Syst, vol.29, issue.6, 2007.

K. Honda, N. Yoshida, and M. Carbone, Multiparty Asynchronous Session Types, POPL 2008, pp.273-284, 2008.
DOI : 10.1145/1328438.1328472

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=

H. Hüttel, I. Lanese, V. T. Vasconcelos, L. Caires, M. Carbone et al., Foundations of behavioural types, 2014.

S. Jaksic, Input/output types for dynamic web data, 2012.

D. Kitchin, A. Quark, W. R. Cook, and J. Misra, The Orc Programming Language, LNCS, vol.4, issue.7, pp.1-25, 2009.
DOI : 10.1007/11817949_32

N. Kobayashi, A Type System for Lock-Free Processes, Information and Computation, vol.177, issue.2, pp.122-159, 2002.
DOI : 10.1016/S0890-5401(02)93171-8

N. Kobayashi, Type-based information flow analysis for the ??-calculus, Acta Informatica, vol.15, issue.2/3, pp.291-347, 2005.
DOI : 10.1007/s00236-005-0179-x

M. Kolundzija, Security Types for Sessions and Pipelines, WS-FM 2008, pp.175-190, 2008.
DOI : 10.3233/JCS-1996-42-304

A. Lapadula, R. Pugliese, and F. Tiezzi, Regulating Data Exchange in Service Oriented Applications, LNCS, vol.4767, pp.223-239, 2007.
DOI : 10.1007/978-3-540-75698-9_15

A. Mukhija, A. Dingwall-smith, and D. Rosenblum, QoS-Aware Service Composition in Dino, Fifth European Conference on Web Services (ECOWS'07), pp.3-12, 2007.
DOI : 10.1109/ECOWS.2007.24

G. C. Necula, Proof-carrying code, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '97, pp.106-119, 1997.
DOI : 10.1145/263699.263712

L. Padovani, Deadlock and lock freedom in the linear ??-calculus, Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS '14, p.72, 2014.
DOI : 10.1145/2603088.2603116

URL : https://hal.archives-ouvertes.fr/hal-00932356

J. A. Pérez, L. Caires, F. Pfenning, and B. Toninho, Linear logical relations and observational equivalences for session-based concurrency, Information and Computation, vol.239, pp.254-302, 2014.
DOI : 10.1016/j.ic.2014.08.001

F. Pfenning, Intensionality, extensionality, and proof irrelevance in modal type theory, Proceedings 16th Annual IEEE Symposium on Logic in Computer Science, pp.221-230, 2001.
DOI : 10.1109/LICS.2001.932499

F. Pfenning, L. Caires, and B. Toninho, Proof-Carrying Code in a Session-Typed Process Calculus, CPP 2011, pp.21-36, 2011.
DOI : 10.1007/978-3-642-11957-6_28

J. Planul, R. Corin, and C. Fournet, Secure Enforcement for Global Process Specifications, CONCUR 2009, pp.511-526, 2009.
DOI : 10.1007/BFb0053567

F. Pottier, A simple view of type-secure information flow in the ??-calculus, Proceedings 15th IEEE Computer Security Foundations Workshop. CSFW-15, pp.320-330, 2002.
DOI : 10.1109/CSFW.2002.1021826

F. Pottier, C. Skalka, and S. F. Smith, A systematic approach to static access control, ACM Transactions on Programming Languages and Systems, vol.27, issue.2, pp.344-382, 2005.
DOI : 10.1145/1057387.1057392

R. Pugliese and F. Tiezzi, A calculus for orchestration of web services, Journal of Applied Logic, vol.10, issue.1, pp.2-31, 2012.
DOI : 10.1016/j.jal.2011.11.002

P. Y. Ryan and S. A. Schneider, Process algebra and non-interference, CSFW 1999, pp.214-227, 1999.

J. F. Santos and T. Rezk, An Information Flow Monitor-Inlining Compiler for Securing a Core of JavaScript, SEC 2014, pp.278-292, 2014.
DOI : 10.1007/978-3-642-55415-5_23

URL : https://hal.archives-ouvertes.fr/hal-01087374

J. Siek and W. Taha, Gradual Typing for Objects, LNCS, vol.4609, pp.2-27, 2007.
DOI : 10.1007/978-3-540-73589-2_2

J. G. Siek and W. Taha, Gradual typing for functional languages, Scheme and Functional Programming Workshop, pp.81-92, 2006.

V. Simonet, The Flow Caml System: Documentation and users manual. INRIA, 2003.

J. Sunshine, K. Naden, S. Stork, J. Aldrich, and . Tanter, First-class state change in Plaid, OOPSLA 2011, pp.713-732, 2011.

N. Swamy, J. Chen, C. Fournet, P. Strub, K. Bhargavan et al., Secure distributed programming with value-dependent types, Journal of Functional Programming, vol.23, issue.04, pp.402-451, 2013.
DOI : 10.1017/S0956796813000142

URL : https://hal.archives-ouvertes.fr/hal-00939188

P. Thiemann, Session Types with Gradual Typing, TGC 2014, pp.144-158, 2014.
DOI : 10.1007/978-3-662-45917-1_10

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=

S. Tobin-hochstadt and M. Felleisen, Interlanguage migration, Companion to the 21st ACM SIGPLAN conference on Object-oriented programming systems, languages, and applications , OOPSLA '06, pp.964-974, 2006.
DOI : 10.1145/1176617.1176755

B. Toninho, L. Caires, and F. Pfenning, Dependent session types via intuitionistic linear type theory, Proceedings of the 13th international ACM SIGPLAN symposium on Principles and practices of declarative programming, PPDP '11, pp.161-172, 2011.
DOI : 10.1145/2003476.2003499

J. A. Tov and R. Pucella, Stateful Contracts for Affine Types, ESOP 2010, pp.550-569, 2010.
DOI : 10.1007/978-3-642-11957-6_29

A. Vallecillo, V. T. Vasconcelos, and A. Ravara, Typing the behavior of software components using session types, Fundam. Inform, vol.73, issue.4, pp.583-598, 2006.

V. T. Vasconcelos, S. J. Gay, and A. Ravara, Type checking a multithreaded functional language with session types, Theoretical Computer Science, vol.368, issue.1-2, pp.64-87, 2006.
DOI : 10.1016/j.tcs.2006.06.028

D. Volpano, C. Irvine, and G. Smith, A sound type system for secure flow analysis, Journal of Computer Security, vol.4, issue.2-3, pp.167-187, 1996.
DOI : 10.3233/JCS-1996-42-304

]. R. Wolff, R. Garcia, ´. E. Tanter, and J. Aldrich, Gradual Typestate, LNCS, vol.12, issue.1, pp.459-483, 2011.
DOI : 10.1109/TSE.1986.6312929

N. Yoshida, R. Hu, R. Neykova, and N. Ng, The Scribble protocol language, TGC 2013, pp.22-41, 2013.