Abstract
This paper describes an approach to the behavioural analysis of sessions. The approach is made possible by the calculus of structures — a deep inference proof calculus, generalising the sequent calculus, where inference rules are applied in any context. The approach involves specifications of global and local sessions inspired by the Scribble language. The calculus features a novel operator that synchronises parts of a protocol that must be treated atomically. Firstly, the calculus can be used to determine whether local sessions can be compose in a type safe fashion such that sessions are capable of successfully completing. Secondly, the calculus defines a subtyping relation for sessions that allows causal dependencies to be weakened while retaining termination potential. Consistency and complexity results follow from proof theory.
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsReferences
Abramsky, S.: Computational interpretations of linear logic. Theoret. Comput. Sci. 111(1), 3–57 (1993)
Benzaken, V., Castagna, G., Frisch, A.: CDuce: an XML-centric general-purpose language. ACM SIGPLAN Not. 38(9), 51–63 (2003)
Caires, L., Pfenning, F.: Session types as intuitionistic linear propositions. In: Gastin, P., Laroussinie, F. (eds.) CONCUR 2010. LNCS, vol. 6269, pp. 222–236. Springer, Heidelberg (2010)
Chaudhuri, K., Guenot, N., Straßburger, L.: The focused calculus of structures. In: EACSL, vol. 12, pp. 159–173 (2011)
Deniélou, P.-M., Yoshida, N.: Multiparty compatibility in communicating automata: characterisation and synthesis of global session types. In: Fomin, F.V., Freivalds, R., Kwiatkowska, M., Peleg, D. (eds.) ICALP 2013, Part II. LNCS, vol. 7966, pp. 174–186. Springer, Heidelberg (2013)
Gay, S., Hole, M.: Subtyping for session types in the pi calculus. Acta Informatica 42(2–3), 191–225 (2005)
Gay, S.J., Vasconcelos, V.T.: Linear type theory for asynchronous session types. J. Funct. Program. 20(1), 19 (2010)
Gischer, J.L.: The equational theory of pomsets. Theoret. Comput. Sci. 61(2–3), 199–224 (1988)
Guglielmi, A.: A system of interaction and structure. ACM Trans. Comput. Logic 8, 1–64 (2007)
Honda, K.: Types for dyadic interaction. In: Best, E. (ed.) CONCUR 1993. LNCS, vol. 715, pp. 509–523. Springer, Heidelberg (1993)
Honda, K., Mukhamedov, A., Brown, G., Chen, T.-C., Yoshida, N.: Scribbling interactions with a formal foundation. In: Natarajan, R., Ojo, A. (eds.) ICDCIT 2011. LNCS, vol. 6536, pp. 55–75. Springer, Heidelberg (2011)
Honda, K., Yoshida, N., Carbone, M.: Multiparty asynchronous session types. ACM SIGPLAN Not. 43(1), 273–284 (2008)
Horne, R.: The consistency and complexity of multiplicative additive system virtual. Sci. Ann. Comput. Sci. XXV(2), 245–316 (2015). doi:10.7561/SACS.2015.2.245
Hu, R., Neykova, R., Yoshida, N., Demangeon, R., Honda, K.: Practical interruptible conversations. In: Legay, A., Bensalem, S. (eds.) RV 2013. LNCS, vol. 8174, pp. 130–148. Springer, Heidelberg (2013)
Hu, R., Yoshida, N., Honda, K.: Session-based distributed programming in java. In: Vitek, J. (ed.) ECOOP 2008. LNCS, vol. 5142, pp. 516–541. Springer, Heidelberg (2008)
Kahramanogullari, O.: Maude as a platform for designing and implementing deep inference systems. ENTCS 219, 35–50 (2008)
Lincoln, P., et al.: Decision problems for propositional linear logic. Ann. Pure Appl. Logic 56(1), 239–311 (1992)
Mostrous, D., Yoshida, N., Honda, K.: Global principal typing in partially commutative asynchronous sessions. In: Castagna, G. (ed.) ESOP 2009. LNCS, vol. 5502, pp. 316–332. Springer, Heidelberg (2009)
Ng, N., Yoshida, N., Honda, K.: Multiparty session C: safe parallel programming with message optimisation. In: Furia, C.A., Nanz, S. (eds.) TOOLS 2012. LNCS, vol. 7304, pp. 202–218. Springer, Heidelberg (2012)
Pierce, B., Sangiorgi, D.: Typing and subtyping for mobile processes. In: LICS 1993, pp. 376–385. IEEE (1993)
Tiu, A.: A system of interaction, structure II: the need for deep inference. Logical Methods Comput. Sci. 2(2), 1–24 (2006)
Wadler, P.: Propositions as sessions. J. Funct. Prog. 24(2–3), 384–418 (2014)
Acknowledgements
This work is supported by a grant of the Romanian National Authority for Scientific Research, project number PN-II-ID-PCE-2011-3-0919. The second author received support from MOE Tier 2 grant MOE2014-T2-2-076.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing Switzerland
About this paper
Cite this paper
Ciobanu, G., Horne, R. (2016). Behavioural Analysis of Sessions Using the Calculus of Structures. In: Mazzara, M., Voronkov, A. (eds) Perspectives of System Informatics. PSI 2015. Lecture Notes in Computer Science(), vol 9609. Springer, Cham. https://doi.org/10.1007/978-3-319-41579-6_8
Download citation
DOI: https://doi.org/10.1007/978-3-319-41579-6_8
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-41578-9
Online ISBN: 978-3-319-41579-6
eBook Packages: Computer ScienceComputer Science (R0)