Skip to main content
SpringerLink
Log in

From Behavioural Contracts to Session Types

  • Chapter
  • First Online:
Models, Languages, and Tools for Concurrent and Distributed Programming

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

  • 685 Accesses

Abstract

We present a research trajectory of the authors and colleagues dealing with the correctness and meaningful composition of software components, trajectory that incrementally traverses successive paradigms and approaches: open distributed processing, contract based reasoning, behavioural typing and session types. This research is grounded on the foundational work of Robin Milner on processes and observation equivalence, and the followup work by De Nicola and Hennessy on testing relations. Indeed, these initial works have set benchmarks that define the meaning of behaviour, which has fostered a full body of research in concurrency and verification. Behavioural typing is one of the avenues opened by these early contributions. This paper is a brief and staged report of the research accomplished by the authors and colleagues, presented in chronological order, starting with their work on the computational model of open distributed processing and ending at their latest work on sessions for web services.

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. Abadi, M., Lamport, L.: Composing specifications. ACM Trans. Program. Lang. Syst. 15(1), 73–132 (1993). https://doi.org/10.1145/151646.151649

    Article  Google Scholar 

  2. de Alfaro, L., Henzinger, T.A.: Interface automata. In: ESEC/FSE-01. Software Engineering Notes, vol. 26, p. 5. ACM Press (2001)

    Google Scholar 

  3. Alrahman, Y.A., De Nicola, R., Loreti, M., Tiezzi, F., Vigo, R.: A calculus for attribute-based communication. In: Wainwright, R.L., Corchado, J.M., Bechini, A., Hong, J. (eds.) Proceedings of the 30th Annual ACM Symposium on Applied Computing, Salamanca, Spain, 13–17 April 2015, pp. 1840–1845. ACM (2015). https://doi.org/10.1145/2695664.2695668

  4. Amadio, R.M., Cardelli, L.: Subtyping recursive types. ACM Trans. Program. Lang. Syst. 15(4), 575–631 (1993). https://doi.org/10.1145/155183.155231

    Article  Google Scholar 

  5. Bernardeschi, C., Dustzadeh, J., Fantechi, A., Najm, E., Nimour, A., Olsen, F.: Consistent semantics and correct transformations for the ODP information and computational models. In: Proceedings of 2nd IFIP Conference on Formal Methods for Open Object-based Distributed Systems (FMOODS). Chapman & Hall, Canterbury, July 1997

    Google Scholar 

  6. Bernardi, G., Hennessy, M.: Using higher-order contracts to model session types. Log. Methods Comput. Sci. 12(2) (2016)

    Google Scholar 

  7. Boreale, M., et al.: 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). https://doi.org/10.1007/11841197_3

    Chapter  Google Scholar 

  8. 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). https://doi.org/10.1007/978-3-540-68863-1_3

    Chapter  Google Scholar 

  9. Boreale, M., Bruni, R., De Nicola, R., Loreti, M.: CaSPiS: a calculus of sessions, pipelines and services. Math. Struct. Comput. Sci. 25(3), 666–709 (2015). https://doi.org/10.1017/S0960129512000953

    Article  MathSciNet  MATH  Google Scholar 

  10. Bravetti, M., Zavattaro, G.: A foundational theory of contracts for multi-party service composition. Fundam. Inf. 89, 451–478 (2008)

    MathSciNet  MATH  Google Scholar 

  11. Bruni, R., Lanese, I., Melgratti, H., Tuosto, E.: Multiparty sessions in SOC. In: Lea, D., Zavattaro, G. (eds.) COORDINATION 2008. LNCS, vol. 5052, pp. 67–82. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-68265-3_5

    Chapter  Google Scholar 

  12. Cardelli, L., Gordon, A.: Mobile ambients. Theor. Comput. Sci. 240(1), 173–213 (2000)

    Article  MathSciNet  Google Scholar 

  13. Carrez, C., Fantechi, A., Najm, E.: Behavioural contracts for a sound assembly of components. In: König, H., Heiner, M., Wolisz, A. (eds.) FORTE 2003. LNCS, vol. 2767, pp. 111–126. Springer, Heidelberg (2003). https://doi.org/10.1007/978-3-540-39979-7_8

    Chapter  MATH  Google Scholar 

  14. Carrez, C., Fantechi, A., Najm, E.: Assembling components with behavioural contracts. Annales des Télécommunications 60(7–8), 989–1022 (2005). https://doi.org/10.1007/BF03219957

    Article  MATH  Google Scholar 

  15. Castagna, G., Gesbert, N., Padovani, L.: A theory of contracts for web services. In: Proceedings of the 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2008, pp. 261–272. ACM, New York (2008). https://doi.org/10.1145/1328438.1328471

  16. Chinnici, R., Moreau, J.J., Ryman, A., Weerawarana, S.: Web Service Definition Language (WSDL) Version 2.0, W3C. Technical report, June 2007

    Google Scholar 

  17. Coppo, M., Dezani-Ciancaglini, M., Padovani, L., Yoshida, N.: Inference of global progress properties for dynamically interleaved multiparty sessions. In: De Nicola, R., Julien, C. (eds.) COORDINATION 2013. LNCS, vol. 7890, pp. 45–59. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-38493-6_4

    Chapter  Google Scholar 

  18. De Nicola, R., Ferrari, G., Loreti, M., Pugliese, R.: A language-based approach to autonomic computing. In: Beckert, B., Damiani, F., de Boer, F.S., Bonsangue, M.M. (eds.) FMCO 2011. LNCS, vol. 7542, pp. 25–48. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-35887-6_2

    Chapter  Google Scholar 

  19. De Nicola, R., Hennessy, M.: Testing equivalences for processes. Theor. Comput. Sci. 34, 83–133 (1984). https://doi.org/10.1016/0304-3975(84)90113-0

    Article  MathSciNet  MATH  Google Scholar 

  20. De Nicola, R., Pugliese, R.: A process algebra based on Linda. In: Ciancarini, P., Hankin, C. (eds.) COORDINATION 1996. LNCS, vol. 1061, pp. 160–178. Springer, Heidelberg (1996). https://doi.org/10.1007/3-540-61052-9_45

    Chapter  Google Scholar 

  21. DeNicola, R., Ferrari, G., Pugliese, R.: KLAIM: a Kernel language for agents interaction and mobility. IEEE Trans. Softw. Eng. 24(5), 315–330 (1998)

    Article  Google Scholar 

  22. Dustzadeh, J., Najm, E.: Consistent semantics for ODP information and computational models. In: Specification, Testing IFIP TC6 WG6.1, Techniques for X) and 18–21 November, 1997, Osaka, Japan. IFIP Conference Proceedings, vol. 107, pp. 107–126. Chapman & Hall (1997)

    Google Scholar 

  23. Fantechi, A., Najm, E.: Session types for orchestration charts. In: Lea, D., Zavattaro, G. (eds.) COORDINATION 2008. LNCS, vol. 5052, pp. 117–134. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-68265-3_8

    Chapter  Google Scholar 

  24. Février, A., Najm, E., Stefani, J.: Contracts for ODP. In: Bertran, M., Rus, T. (eds.) Transformation-Based Reactive Systems Development. Springer, Heidelberg (1997). https://doi.org/10.1007/3-540-63010-4_15

    Chapter  Google Scholar 

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

    Article  MathSciNet  Google Scholar 

  26. Gay, S., Hole, M.: Types and subtypes for client-server interactions. In: Swierstra, S.D. (ed.) ESOP 1999. LNCS, vol. 1576, pp. 74–90. Springer, Heidelberg (1999). https://doi.org/10.1007/3-540-49099-X_6

    Chapter  Google Scholar 

  27. Hennessy, M., Rathke, J., Yoshida, N.: SafeDpi: a language for controlling mobile code. Acta Inf. 42(4–5), 227–290 (2005)

    Article  MathSciNet  Google Scholar 

  28. Honda, K., Yoshida, N., Carbone, M.: Multiparty asynchronous session types. SIGPLAN Not. 43, 273–284 (2008). https://doi.org/10.1145/1328897.1328472

    Article  MATH  Google Scholar 

  29. Hüttel, H., et al.: Foundations of session types and behavioural contracts. ACM Comput. Surv. 49(1), 3:1–3:36 (2016). https://doi.org/10.1145/2873052

    Article  Google Scholar 

  30. ISO, IEC: Information Technology Open Distributed Processing Reference Model. IS 10746 parts 1,2,3 (1998–2010), also published as ITU-T Recommendations X901, X.902, X.903

    Google Scholar 

  31. Kitchin, D., Cook, W.R., Misra, J.: A language for task orchestration and its semantic properties. In: Baier, C., Hermanns, H. (eds.) CONCUR 2006. LNCS, vol. 4137, pp. 477–491. Springer, Heidelberg (2006). https://doi.org/10.1007/11817949_32

    Chapter  Google Scholar 

  32. Kitchin, D., Quark, A., Cook, W., Misra, J.: The orc programming language. In: Lee, D., Lopes, A., Poetzsch-Heffter, A. (eds.) FMOODS/FORTE -2009. LNCS, vol. 5522, pp. 1–25. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-02138-1_1

    Chapter  Google Scholar 

  33. Lanese, I., Martins, F., Vasconcelos, V.T., Ravara, A.: Disciplining orchestration and conversation in service-oriented computing. In: Proceedings of the Fifth IEEE International Conference on Software Engineering and Formal Methods, SEFM 2007, pp. 305–314. IEEE Computer Society, Washington, DC (2007), https://doi.org/10.1109/SEFM.2007.13

  34. 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). https://doi.org/10.1007/978-3-540-71316-6_4

    Chapter  Google Scholar 

  35. Lapadula, A., Pugliese, R., Tiezzi, F.: A WSDL-based type system for asynchronous WS-BPEL processes. Form. Methods Syst. Des. 38(2), 119–157 (2011). https://doi.org/10.1007/s10703-010-0110-0

    Article  MATH  Google Scholar 

  36. Larsen, K.G., Steffen, B., Weise, C.: A constraint oriented proof methodology based on modal transition systems. In: Brinksma, E., Cleaveland, W.R., Larsen, K.G., Margaria, T., Steffen, B. (eds.) TACAS 1995. LNCS, vol. 1019, pp. 17–40. Springer, Heidelberg (1995). https://doi.org/10.1007/3-540-60630-0_2

    Chapter  Google Scholar 

  37. Levi, F., Sangiorgi, D.: Mobile safe ambients. ACM. Trans. Program. Lang. Syst. 25(1), 1–69 (2003)

    Article  Google Scholar 

  38. Meseguer, J.: Conditioned rewriting logic as a united model of concurrency. Theor. Comput. Sci. 96(1), 73–155 (1992). https://doi.org/10.1016/0304-3975(92)90182-F

    Article  MATH  Google Scholar 

  39. Michaux, J., Najm, E., Fantechi, A.: Session types for safe web service orchestration. J. Log. Algebr. Program. 82(8), 282–310 (2013). https://doi.org/10.1016/j.jlap.2013.05.004

    Article  MathSciNet  MATH  Google Scholar 

  40. Milner, R.: The Space and Motion of Communicating Agents. Cambridge University Press, Cambridge (2009)

    Book  Google Scholar 

  41. Milner, R., Parrow, J., Walker, J.: A calculus of mobile processes, I. Inf. Comput. 100(1), 1–40 (1992). Technical report ECS-LFCS-89-85

    Article  MathSciNet  Google Scholar 

  42. Milner, R., Parrow, J., Walker, J.: A calculus of mobile processes, II. Inf. Comput. 100(1), 41–77 (1992). Technical report ECS-LFCS-89-86

    Article  MathSciNet  Google Scholar 

  43. Milner, R.: A Calculus of Communicating Systems. Lecture Notes in Computer Science, vol. 158. Springer, Heidelberg (1983)

    MATH  Google Scholar 

  44. Mostrous, D., Vasconcelos, V.T.: Session typing for a featherweight erlang. In: De Meuter, W., Roman, G.-C. (eds.) COORDINATION 2011. LNCS, vol. 6721, pp. 95–109. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-21464-6_7

    Chapter  Google Scholar 

  45. Najm, E., Nimour, A.: A calculus of object bindings. In: Proceedings of 2nd IFIP Conference on Formal Methods for Open Object-based Distributed Systems (FMOODS). Chapman & Hall, Canterbury, July 1997

    Google Scholar 

  46. Najm, E., Stefani, J.: A formal semantics of DPL. Technical report, Report CNET/RC.V01.ENJBS.004., Esprit Project 2267 (Integrated Systems Architecture) (1992)

    Google Scholar 

  47. Najm, E., Nimour, A., Stefani, J.-B.: Guaranteeing liveness in an object calculus through behavioral typing. In: Wu, J., Chanson, S.T., Gao, Q. (eds.) Formal Methods for Protocol Engineering and Distributed Systems. IAICT, vol. 28, pp. 203–221. Springer, Boston (1999). https://doi.org/10.1007/978-0-387-35578-8_12

    Chapter  MATH  Google Scholar 

  48. Najm, E., Nimour, A., Stefani, J.-B.: Infinite types for distributed object interfaces. In: Ciancarini, P., Fantechi, A., Gorrieri, R. (eds.) FMOODS 1999. ITIFIP, vol. 10, pp. 353–369. Springer, Boston, MA (1999). https://doi.org/10.1007/978-0-387-35562-7_28

    Chapter  MATH  Google Scholar 

  49. Najm, E., Stefani, J.: A formal semantics for the ODP computational model. Comput. Netw. ISDN Syst. 27(8), 1305–1329 (1995). https://doi.org/10.1016/0169-7552(94)00032-O

    Article  Google Scholar 

  50. Ng, N., Yoshida, N., Pernet, O., Hu, R., Kryftis, Y.: Safe parallel programming with session java. In: De Meuter, W., Roman, G.-C. (eds.) COORDINATION 2011. LNCS, vol. 6721, pp. 110–126. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-21464-6_8

    Chapter  Google Scholar 

  51. O’Hearn, P.W.: A primer on separation logic (and automatic program verification and analysis). In: Software Safety and Security - Tools for Analysis and Verification, NATO Science for Peace and Security Series - D: Information and Communication Security, vol. 33. IOS Press (2012)

    Google Scholar 

  52. Organization for the Advancement of Structured Information Standards (OASIS): Web Services Business Process Execution Language (WS-BPEL) Version 2.0, April 2007

    Google Scholar 

  53. Schmitt, A., Stefani, J.-B.: The kell calculus: a family of higher-order distributed process calculi. In: Priami, C., Quaglia, P. (eds.) GC 2004. LNCS, vol. 3267, pp. 146–178. Springer, Heidelberg (2005). https://doi.org/10.1007/978-3-540-31794-4_9

    Chapter  Google Scholar 

  54. Sevegnani, M., Calder, M.: Bigraphs with sharing. Theor. Comput. Sci. 577, 43–73 (2015). https://doi.org/10.1016/j.tcs.2015.02.011

    Article  MathSciNet  MATH  Google Scholar 

  55. Uriarte, R.B., Tiezzi, F., De Nicola, R.: SLAC: a formal service-level-agreement language for cloud computing. In: Proceedings of the 7th IEEE/ACM International Conference on Utility and Cloud Computing, UCC 2014, London, United Kingdom, 8–11 December 2014, pp. 419–426. IEEE Computer Society (2014). https://doi.org/10.1109/UCC.2014.53

  56. Vallecillo, A., Vasconcelos, V.T., Ravara, A.: Typing the behavior of software components using session types. Fundam. Inf. 73(4), 583–598 (2006)

    MathSciNet  MATH  Google Scholar 

  57. Yoshida, N., Vasconcelos, V.T.: Language primitives and type discipline for structured communication-based programming revisited: two systems for higher-order session communication. Electron. Notes Theor. Comput. Sci. 171(4), 73–93 (2007). https://doi.org/10.1016/j.entcs.2007.02.056

    Article  Google Scholar 

Download references

Acknowledgments

The work reported in the present paper has been carried out over the years by a group of authors: Arnaud Bailly, Cinzia Bernardeschi, Cyril Carrez, Joubine Dustzadeh, Alessandro Fantechi, Arnaud Février, Jonathan Michaux, Elie Najm, Abdelkrim Nimour, Frank Olsen, Jean-Bernard Stefani.

Author information

Authors and Affiliations

  1. Università di Firenze, Florence, Italy

    Alessandro Fantechi

  2. Institut Polytechnique de Paris, Telecom Paris, LTCI, Paris, France

    Elie Najm

  3. INRIA, Rocquencourt, France

    Jean-Bernard Stefani

Authors
  1. Alessandro Fantechi
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Elie Najm
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Jean-Bernard Stefani
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Elie Najm .

Editor information

Editors and Affiliations

  1. Department of Statistics, Computer Science, Applications, University of Florence, Florence, Italy

    Michele Boreale

  2. School of Science and Technology, University of Camerino, Camerino, Italy

    Flavio Corradini

  3. School of Science and Technology, University of Camerino, Camerino, Italy

    Michele Loreti

  4. Department of Statistics, Computer Science, Applications, University of Florence, Florence, Italy

    Rosario Pugliese

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this chapter

Check for updates. Verify currency and authenticity via CrossMark

Cite this chapter

Fantechi, A., Najm, E., Stefani, JB. (2019). From Behavioural Contracts to Session Types. In: Boreale, M., Corradini, F., Loreti, M., Pugliese, R. (eds) Models, Languages, and Tools for Concurrent and Distributed Programming. Lecture Notes in Computer Science(), vol 11665. Springer, Cham. https://doi.org/10.1007/978-3-030-21485-2_16

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-21485-2_16

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-21484-5

  • Online ISBN: 978-3-030-21485-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation