Using Higher-Order Contracts to Model Session Types (Extended Abstract)

  • Giovanni Bernardi
  • Matthew Hennessy
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8704)


Session types are used to describe and structure interactions between independent processes in distributed systems. Higher-order types are needed in order to properly structure delegation of responsibility between processes. In this paper we show that higher-order web-service contracts can be used to provide a fully-abstract model of recursive higher-order session types. The model is set-theoretic, in the sense that the denotation of a contract is given by the set of contracts with which it complies; we use a novel notion of peer compliance. A crucial step in the proof of full-abstraction is showing that every contract has a non-empty denotation.


Source Language Session Type Type Duality Process Calculus Happy State 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Barbanera, F., de’Liguoro, U.: Two notions of sub-behaviour for session-based client/server systems. In: Kutsia, T., Schreiner, W., Fernández, M. (eds.) PPDP, pp. 155–164. ACM (2010)Google Scholar
  2. 2.
    Barbanera, F., de’Liguoro, U.: Sub-behaviour relations for session-based client/server systems (2013) (submitted for publication)Google Scholar
  3. 3.
    Bernardi, G.: Behavioural Equivalences for Web Services. Ph.D. thesis, Trinity College Dublin (2013),
  4. 4.
    Bernardi, G., Hennessy, M.: Modelling session types using contracts. In: Ossowski, S., Lecca, P. (eds.) SAC, pp. 1941–1946. ACM (2012)Google Scholar
  5. 5.
    Bernardi, G., Hennessy, M.: Using higher-order contracts to model session types. CoRR abs/1310.6176 (2013)Google Scholar
  6. 6.
    Bono, V., Padovani, L.: Typing copyless message passing. Logical Methods in Computer Science 8(1) (2012)Google Scholar
  7. 7.
    Castagna, G., De Nicola, R., Varacca, D.: Semantic subtyping for the pi-calculus. Theor. Comput. Sci. 398(1-3), 217–242 (2008)CrossRefzbMATHGoogle Scholar
  8. 8.
    Castagna, G., Dezani-Ciancaglini, M., Giachino, E., Padovani, L.: Foundations of session types. In: Porto, A., López-Fraguas, F.J. (eds.) PPDP, pp. 219–230. ACM (2009)Google Scholar
  9. 9.
    Castagna, G., Gesbert, N., Padovani, L.: A theory of contracts for web services. ACM Trans. Program. Lang. Syst. 31(5), 1–61 (2009), Supersedes the article in POPL 2008Google Scholar
  10. 10.
    De Nicola, R., Hennessy, M.: Testing equivalences for processes. Theoretical Computer Science 34, 83–133 (1984)CrossRefzbMATHMathSciNetGoogle Scholar
  11. 11.
    Dezani-Ciancaglini, M., de’Liguoro, U.: Sessions and session types: An overview. In: Laneve, C., Su, J. (eds.) WS-FM 2009. LNCS, vol. 6194, pp. 1–28. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  12. 12.
    Frisch, A., Castagna, G., Benzaken, V.: Semantic subtyping: Dealing set-theoretically with function, union, intersection, and negation types. J. ACM 55(4), 19:1–19:64 (2008),
  13. 13.
    Gay, S.J., Hole, M.: Subtyping for session types in the pi calculus. Acta Inf. 42(2-3), 191–225 (2005)CrossRefzbMATHMathSciNetGoogle Scholar
  14. 14.
    Hoare, C.A.R.: Communicating sequential processes. Prentice-Hall (1985)Google Scholar
  15. 15.
    Honda, K., Vasconcelos, V.T., Kubo, M.: Language primitives and type discipline for structured communication-based programming. In: Hankin, C. (ed.) ESOP 1998. LNCS, vol. 1381, pp. 122–138. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  16. 16.
    Laneve, C., Padovani, L.: The must preorder revisited. In: Caires, L., Vasconcelos, V.T. (eds.) CONCUR 2007. LNCS, vol. 4703, pp. 212–225. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  17. 17.
    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)CrossRefGoogle Scholar
  18. 18.
    Milner, R.: Communication and concurrency. PHI Series in computer science. Prentice Hall (1989)Google Scholar
  19. 19.
    Padovani, L.: Contract-based discovery of web services modulo simple orchestrators. Theor. Comput. Sci. 411(37), 3328–3347 (2010)CrossRefzbMATHMathSciNetGoogle Scholar
  20. 20.
    Padovani, L.: Fair Subtyping for Multi-Party Session Types. In: De Meuter, W., Roman, G.-C. (eds.) COORDINATION 2011. LNCS, vol. 6721, pp. 127–141. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  21. 21.
    Takeuchi, K., Honda, K., Kubo, M.: An interaction-based language and its typing system. In: Halatsis, C., Maritsas, D., Philokyprou, G., Theodoridis, S. (eds.) PARLE 1994. LNCS, vol. 817, pp. 398–413. Springer, Heidelberg (1994)CrossRefGoogle Scholar
  22. 22.
    Vasconcelos, V.T.: Fundamentals of session types. Inf. Comput. 217, 52–70 (2012)CrossRefzbMATHMathSciNetGoogle Scholar
  23. 23.
    Yoshida, N., Vasconcelos, V.T.: Language primitives and type discipline for structured communication-based programming revisited: Two systems for higher-order session communication. Electr. Notes Theor. Comput. Sci. 171(4), 73–93 (2007)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2014

Authors and Affiliations

  • Giovanni Bernardi
    • 1
  • Matthew Hennessy
    • 2
  1. 1.IMDEA Software InstituteMadridSpain
  2. 2.School of Computer Science and StatisticsUniversity of Dublin, Trinity CollegeIreland

Personalised recommendations