Skip to main content
SpringerLink
Log in

Behavioural Analysis of Sessions Using the Calculus of Structures

  • Conference paper
  • First Online:
Perspectives of System Informatics (PSI 2015)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 9609))

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

References

  1. Abramsky, S.: Computational interpretations of linear logic. Theoret. Comput. Sci. 111(1), 3–57 (1993)

    Article  MathSciNet  MATH  Google Scholar 

  2. Benzaken, V., Castagna, G., Frisch, A.: CDuce: an XML-centric general-purpose language. ACM SIGPLAN Not. 38(9), 51–63 (2003)

    Article  MATH  Google Scholar 

  3. 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)

    Chapter  Google Scholar 

  4. Chaudhuri, K., Guenot, N., Straßburger, L.: The focused calculus of structures. In: EACSL, vol. 12, pp. 159–173 (2011)

    Google Scholar 

  5. 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)

    Google Scholar 

  6. Gay, S., Hole, M.: Subtyping for session types in the pi calculus. Acta Informatica 42(2–3), 191–225 (2005)

    Article  MathSciNet  MATH  Google Scholar 

  7. Gay, S.J., Vasconcelos, V.T.: Linear type theory for asynchronous session types. J. Funct. Program. 20(1), 19 (2010)

    Article  MathSciNet  MATH  Google Scholar 

  8. Gischer, J.L.: The equational theory of pomsets. Theoret. Comput. Sci. 61(2–3), 199–224 (1988)

    Article  MathSciNet  MATH  Google Scholar 

  9. Guglielmi, A.: A system of interaction and structure. ACM Trans. Comput. Logic 8, 1–64 (2007)

    Article  MathSciNet  Google Scholar 

  10. Honda, K.: Types for dyadic interaction. In: Best, E. (ed.) CONCUR 1993. LNCS, vol. 715, pp. 509–523. Springer, Heidelberg (1993)

    Google Scholar 

  11. 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)

    Chapter  Google Scholar 

  12. Honda, K., Yoshida, N., Carbone, M.: Multiparty asynchronous session types. ACM SIGPLAN Not. 43(1), 273–284 (2008)

    Article  MATH  Google Scholar 

  13. 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

    MathSciNet  Google Scholar 

  14. 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)

    Chapter  Google Scholar 

  15. 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)

    Chapter  Google Scholar 

  16. Kahramanogullari, O.: Maude as a platform for designing and implementing deep inference systems. ENTCS 219, 35–50 (2008)

    MATH  Google Scholar 

  17. Lincoln, P., et al.: Decision problems for propositional linear logic. Ann. Pure Appl. Logic 56(1), 239–311 (1992)

    Article  MathSciNet  MATH  Google Scholar 

  18. 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)

    Chapter  Google Scholar 

  19. 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)

    Chapter  Google Scholar 

  20. Pierce, B., Sangiorgi, D.: Typing and subtyping for mobile processes. In: LICS 1993, pp. 376–385. IEEE (1993)

    Google Scholar 

  21. Tiu, A.: A system of interaction, structure II: the need for deep inference. Logical Methods Comput. Sci. 2(2), 1–24 (2006)

    Article  MathSciNet  MATH  Google Scholar 

  22. Wadler, P.: Propositions as sessions. J. Funct. Prog. 24(2–3), 384–418 (2014)

    Article  MathSciNet  MATH  Google Scholar 

Download references

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

  1. Institute of Computer Science, Romanian Academy, Iasi, Romania

    Gabriel Ciobanu & Ross Horne

  2. Faculty of Information Technology, Kazakh-British Technical University, Almaty, Kazakhstan

    Ross Horne

  3. School of Computer Science and Engineering, Nanyang Technological University, Singapore City, Singapore

    Ross Horne

Authors
  1. Gabriel Ciobanu
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Ross Horne
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Ross Horne .

Editor information

Editors and Affiliations

  1. Innopolis University, Innopolis, Russia

    Manuel Mazzara

  2. The University of Manchester, Manchester, United Kingdom

    Andrei Voronkov

Rights and permissions

Reprints 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)

Publish with us

Policies and ethics

Search

Navigation