Skip to main content
Springer Nature Link
Log in

Sessions and Session Types: An Overview

  • Conference paper
Web Services and Formal Methods (WS-FM 2009)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 6194))

Included in the following conference series:

Abstract

We illustrate the concepts of sessions and session types as they have been developed in the setting of the π-calculus. Motivated by the goal of obtaining a formalisation closer to existing standards and aiming at their enhancement and strengthening, several extensions of the original core system have been proposed, which we survey together with the embodying of sessions into functional and object-oriented languages, as well as some implementations.

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

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
CHF34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
CHF 24.95
Price includes VAT (Switzerland)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
CHF 47.00
Price excludes VAT (Switzerland)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
CHF 59.00
Price excludes VAT (Switzerland)
  • 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

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

  • Abadi, M., Cardelli, L.: A Theory of Objects. Springer, Heidelberg (1996)

    MATH  Google Scholar 

  • Boreale, M., Bruni, R., Caires, L., De Nicola, R., Lanese, I., Loreti, M., Martins, F., Montanari, U., Ravara, A., Sangiorgi, D., Vasconcelos, V., Zavattaro, G.: SCC: a Service Centered Calculus. In: Bravetti, M., Núñez, M., Zavattaro, G. (eds.) WS-FM 2006. LNCS, vol. 4184, pp. 38–57. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  • Boreale, M., Bruni, R., De Nicola, R., Loreti, M.: Sessions and Pipelines for Structured Service Programming. In: Barthe, G., de Boer, F.S. (eds.) FMOODS 2008. LNCS, vol. 5051, pp. 19–38. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  • Bugliesi, M., Castagna, G., Crafa, S.: Access Control for Mobile Agents: The Calculus of Boxed Ambients. ACM Transactions on Programming Languages and Systems 26(1), 57–124 (2004)

    Article  Google Scholar 

  • Bettini, L., Coppo, M., D’Antoni, L., De Luca, M., Dezani-Ciancaglini, M., Yoshida, N.: Global Progress in Dynamically Interleaved Multiparty Sessions. In: van Breugel, F., Chechik, M. (eds.) CONCUR 2008. LNCS, vol. 5201, pp. 418–433. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  • Bhargavan, K., Corin, R., Deniélou, P.-M., Fournet, C., Leifer, J.J.: Cryptographic Protocol Synthesis and Verification for Multiparty Sessions. In: CSF 2009, pp. 124–140. IEEE Computer Society, Los Alamitos (2009)

    Google Scholar 

  • Bettini, L., Capecchi, S., Dezani-Ciancaglini, M., Giachino, E., Venneri, B.: Session and Union Types for Object Oriented Programming. In: Degano, P., De Nicola, R., Meseguer, J. (eds.) Concurrency, Graphs and Models. LNCS, vol. 5065, pp. 659–680. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  • Barbanera, F., Capecchi, S., de’Liguoro, U.: Typing Asymmetric Client-Server Interaction. In: Sirjani, M. (ed.) FSEN 2009. LNCS, vol. 5961, pp. 97–112. Springer, Heidelberg (2010)

    Google Scholar 

  • Bonelli, E., Compagnoni, A., Gunter, E.: Correspondence Assertions for Process Synchronization in Concurrent Communications. Journal of Functional Programming 15(2), 219–248 (2005)

    Article  MATH  MathSciNet  Google Scholar 

  • Buscemi, M., Montanari, U.: CC-Pi: A Constraint-Based Language for Specifying Service Level Agreements. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 18–32. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  • Buscemi, M., Montanari, U.: Open Bisimulation for the Concurrent Constraint Pi-Calculus. In: Drossopoulou, S. (ed.) ESOP 2008. LNCS, vol. 4960, pp. 254–268. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  • Boreale, M.: On the Expressiveness of Internal Mobility in Name-Passing Calculi. Theoretical Computer Science 195(2), 205–226 (1998)

    Article  MATH  MathSciNet  Google Scholar 

  • Bruce, K.: Foundations of Object-Oriented Languages: Types and Semantics. MIT Press, Cambridge (2002)

    Google Scholar 

  • Berger, M., Yoshida, N., Honda, K.: Completeness and Logical Full Abstraction in Modal Logics for Typed Mobile Processes. In: Aceto, L., Damgård, I., Goldberg, L.A., Halldórsson, M.M., Ingólfsdóttir, A., Walukiewicz, I. (eds.) ICALP 2008, Part II. LNCS, vol. 5126, pp. 99–111. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  • Bravetti, M., Zavattaro, G.: Towards a Unifying Theory for Choreography Conformance and Contract Compliance. In: Lumpe, M., Vanderperren, W. (eds.) SC 2007. LNCS, vol. 4829, pp. 34–50. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  • Capecchi, S., Coppo, M., Dezani-Ciancaglini, M., Drossopoulou, S., Giachino, E.: Amalgamating Sessions and Methods in Object Oriented Languages with Generics. Theoretical Computer Science 410, 142–167 (2009)

    Article  MATH  MathSciNet  Google Scholar 

  • Capecchi, S., Castellani, I., Dezani, M., Rezk, T.: Session Types for Access and Information Flow Control (2009), http://www.di.unito.it/~dezani/ccdr.pdf

  • Coppo, M., Dezani-Ciancaglini, M.: Structured Communications with Concurrent Constraints. In: Kaklamanis, C., Nielson, F. (eds.) TGC 2008. LNCS, vol. 5474, pp. 104–125. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  • Castagna, G., Dezani-Ciancaglini, M., Giachino, E., Padovani, L.: Foundations of Session Types. In: PPDP 2009, pp. 219–230. ACM Press, New York (2009)

    Chapter  Google Scholar 

  • Castagna, G., Frisch, A.: A Gentle Introduction to Semantic Subtyping. In: PPDP 2005, pp. 198–208. ACM Press, New York (2005) (full version); Caires, L., Italiano, G.F., Monteiro, L., Palamidessi, C., Yung, M. (eds.) ICALP 2005. LNCS, vol. 3580, pp. 30–34. Springer, Heidelberg (2005) Joint ICALP-PPDP keynote talk.

    Chapter  Google Scholar 

  • Castagna, G., Gesbert, N., Padovani, L.: A Theory of Contracts for Web Services. ACM Transactions on Programming Languages and Systems article n.19, 31(5), p. 51 (2009)

    Article  Google Scholar 

  • Carbone, M., Honda, K., Yoshida, N.: Structured Communication-Centred Programming for Web Services. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 2–17. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  • Carbone, M., Honda, K., Yoshida, N.: Structured Interactional Exceptions for Session Types. In: van Breugel, F., Chechik, M. (eds.) CONCUR 2008. LNCS, vol. 5201, pp. 402–417. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  • Clarke, D., Noble, J., Potter, J.: Simple Ownership Types for Object Containment. In: Knudsen, J.L. (ed.) ECOOP 2001. LNCS, vol. 2072, pp. 53–76. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  • Castagna, G., Padovani, L.: Contracts for Mobile Processes. In: Bravetti, M., Zavattaro, G. (eds.) CONCUR 2009. LNCS, vol. 5710, pp. 211–228. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  • Caires, L., Vieira, H.T.: Conversation Types. In: Castagna, G. (ed.) ESOP 2009. LNCS, vol. 5502, pp. 285–300. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  • Dezani-Ciancaglini, M., de’ Liguoro, U., Yoshida, N.: On Progress for Structured Communications. In: Barthe, G., Fournet, C. (eds.) TGC 2007 and FODO 2008. LNCS, vol. 4912, pp. 257–275. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  • Dezani-Ciancaglini, M., Drossopoulou, S., Mostrous, D., Yoshida, N.: Session Types for Object-Oriented Languages. Information and Computation 207(5), 595–641 (2009)

    Article  MATH  MathSciNet  Google Scholar 

  • De Nicola, R., Hennessy, M.: CCS Without τ’s. In: Ehrig, H., Levi, G., Montanari, U. (eds.) CAAP 1987 and TAPSOFT 1987. LNCS, vol. 249, pp. 138–152. Springer, Heidelberg (1987)

    Google Scholar 

  • Fähndrich, M., Aiken, M., Hawblitzel, C., Hodson, O., Hunt, G.C., Larus, J.R., Levi, S.: Language Support for Fast and Reliable Message-based Communication in Singularity OS. In: EuroSys 2006, ACM SIGOPS, pp. 177–190. ACM Press, New York (2006)

    Google Scholar 

  • Gay, S.: Bounded Polymorphism in Session Types. Mathematical Structures in Computer Science 18(5), 895–930 (2007)

    Article  MathSciNet  Google Scholar 

  • Gay, S., Gesbert, N., Ravara, A.: Session Types as Generic Process Types. In: PLACES 2008, pp. 16–21 (2008), http://gloss.di.fc.ul.pt/places08/Places08Proceedings.pdf

  • Gay, S., Hole, M.: Subtyping for Session Types in the Pi-Calculus. Acta Informatica 42(2/3), 191–225 (2005)

    Article  MATH  MathSciNet  Google Scholar 

  • Gay, S., Vasconcelos, V.: Linear Type Theory for Asynchronous Session Types. Journal of Functional Programming 20(1), 19–50 (2010)

    Article  MATH  Google Scholar 

  • Gay, S., Vasconcelos, V., Ravara, A., Gesbert, N., Caldeira, A.: Modular Session Types for Distributed Object-Oriented Programming. In: POPL 2010, pp. 299–312. ACM Press, New York (2010)

    Chapter  Google Scholar 

  • Honda, K., Mostrous, D., Yoshida, N.: Global Principal Typing in Partially Commutative Asynchronous Sessions. In: Castagna, G. (ed.) ESOP 2009. LNCS, vol. 5502, pp. 316–332. Springer, Heidelberg (2009)

    Google Scholar 

  • Honda, K., Vasconcelos, V., Kubo, M.: Language Primitives and Type Disciplines for Structured Communication-based Programming. In: Hankin, C. (ed.) ESOP 1998. LNCS, vol. 1381, pp. 122–138. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  • Honda, K., Yoshida, N., Carbone, M.: Multiparty Asynchronous Session Types. In: POPL 2008, pp. 273–284. ACM, New York (2008)

    Chapter  Google Scholar 

  • 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 

  • Igarashi, A., Kobayashi, N.: A Generic Type System for the Pi-Calculus. Theoretical Computer Science 311(1-3), 121–163 (2004)

    Article  MATH  MathSciNet  Google Scholar 

  • Jones, S.P., Gordon, A., Finne, S.: Concurrent Haskell. In: POPL 1996, pp. 295–308. ACM Press, New York (1996)

    Chapter  Google Scholar 

  • Kobayashi, N.: A Partially Deadlock-Free Typed Process Calculus. ACM Transactions on Programming Languages and Systems 20(2), 436–482 (1998)

    Article  Google Scholar 

  • Kobayashi, N.: A Type System for Lock-Free Processes. Information and Computation 177, 122–159 (2002)

    MATH  MathSciNet  Google Scholar 

  • Kobayashi, N.: Type Systems for Concurrent Programs. In: Aichernig, B.K., Maibaum, T. (eds.) Formal Methods at the Crossroads. LNCS, vol. 2757, pp. 439–453. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  • Kobayashi, N.: Type-Based Information Flow Analysis for the Pi-Calculus. Acta Informatica 42(4-5), 291–347 (2005)

    Article  MATH  MathSciNet  Google Scholar 

  • Kobayashi, N.: A New Type System for Deadlock-Free Processes. In: Baier, C., Hermanns, H. (eds.) CONCUR 2006. LNCS, vol. 4137, pp. 233–247. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  • Kobayashi, N.: Type Systems for Concurrent Programs. In: Extended version of [Kob03], Tohoku University (2007)

    Google Scholar 

  • Laneve, C., Padovani, L.: The Pairing of Contracts and Session Types. In: Degano, P., De Nicola, R., Meseguer, J. (eds.) Concurrency, Graphs and Models. LNCS, vol. 5065, pp. 681–700. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  • López, H., Pérez, J., Olarte, C.: Towards a Unified Framework for Declarative Structured Communications. In: PLACES 2009. EPTCS, vol. 17, pp. 1–16 (2010)

    Google Scholar 

  • Lapadula, A., Pugliese, R., Tiezzi, F.: A Calculus for Orchestration of Web Services. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 33–47. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  • Meredith, G., Bjorg, S.: Contracts and Types. Communications of the ACM 46(10), 41–47 (2003)

    Article  Google Scholar 

  • Mostrous, D., Yoshida, N.: Two Sessions Typing Systems for Higher-Order Mobile Processes. In: Della Rocca, S.R. (ed.) TLCA 2007. LNCS, vol. 4583, pp. 321–335. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  • Mostrous, D., Yoshida, N.: A Session Object Calculus for Structured Communication-Based Programming (2008), http://www.doc.ic.ac.uk/~mostrous/sesobj.pdf

  • Mostrous, D., Yoshida, N.: Session-Based Communication Optimisation for Higher-Order Mobile Processes. In: Curien, P.-L. (ed.) TLCA 2009. LNCS, vol. 5608, pp. 203–218. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  • Neubauer, M., Thiemann, P.: An Implementation of Session Types. In: Jayaraman, B. (ed.) PADL 2004. LNCS, vol. 3057, pp. 56–70. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  • Olarte, C., Valencia, F.: Universal Concurrent Constraint Programming: Symbolic Semantics and Applications to Security. In: SAC 2008, pp. 145–150. ACM, New York (2008)

    Chapter  Google Scholar 

  • Padovani, L.: Session Types at the Mirror. In: ICE 2009. EPTCS, vol. 12, pp. 71–86 (2009)

    Google Scholar 

  • Reppy, J.H.: Concurrent Programming in ML. Cambridge University Press, Cambridge (1999)

    Book  Google Scholar 

  • Sackman, M., Eisenbach, S.: Session Types in Haskell (Updating Message Passing for the 21st Century) (2008), http://pubs.doc.ic.ac.uk/session-types-in-haskell/session-types-in-haskell.pdf

  • Sangiorgi, D., Walker, D.: The π-Calculus: a Theory of Mobile Processes. Cambridge University Press, Cambridge (2001)

    Google Scholar 

  • Takeuchi, K., Honda, K., Kubo, M.: An Interaction-based Language and its Typing System. In: Halatsis, C., Philokyprou, G., Maritsas, D., Theodoridis, S. (eds.) PARLE 1994. LNCS, vol. 817, pp. 398–413. Springer, Heidelberg (1994)

    Google Scholar 

  • Vasconcelos, V.: Fundamentals of Session Types. In: Bernardo, M., Padovani, L., Zavattaro, G. (eds.) SFM 2009. LNCS, vol. 5569, pp. 158–186. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  • Vasconcelos, V.: Session Types for Linear Multithreaded Functional Programming. In: PPDP 2009, pp. 1–6. ACM Press, New York (2009)

    Chapter  Google Scholar 

  • Vasconcelos, V., Gay, S., Ravara, A.: Typechecking a Multithreaded Functional Language with Session Types. Theoretical Computer Science 368, 64–87 (2006)

    Article  MATH  MathSciNet  Google Scholar 

  • Vasconcelos, V., Gay, S., Ravara, A., Gesbert, N., Caldeira, A.: Dynamic Interfaces. In: FOOL 2009 (2009), http://www.cs.cmu.edu/~aldrich/FOOL09/vasconcelos.pdf

  • Yoshida, N., Vasconcelos, V.: Language Primitives and Type Disciplines for Structured Communication-based Programming Revisited. In: SecReT 2006. ENTCS, vol. 171, pp. 73–93. Elsevier, Amsterdam (2007)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Dipartimento di Informatica, Università di Torino, corso Svizzera 185, 10149, Torino, Italy

    Mariangiola Dezani-Ciancaglini & Ugo de’Liguoro

Authors
  1. Mariangiola Dezani-Ciancaglini
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Ugo de’Liguoro
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Dipartimento de Scienze dell’Informazione, Mura Anteo, Zamboni 7, Bologna, Italy

    Cosimo Laneve

  2. Department of Computer Science, University of California at Santa Barbara, CA 93106-5110, Santa Barbara, USA

    Jianwen Su

Rights and permissions

Reprints and permissions

Copyright information

© 2010 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Dezani-Ciancaglini, M., de’Liguoro, U. (2010). Sessions and Session Types: An Overview. In: Laneve, C., Su, J. (eds) Web Services and Formal Methods. WS-FM 2009. Lecture Notes in Computer Science, vol 6194. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-14458-5_1

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-14458-5_1

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-14457-8

  • Online ISBN: 978-3-642-14458-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation

  NODES
INTERN 2
Note 3