The Pairing of Contracts and Session Types

  • Cosimo Laneve
  • Luca Padovani
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5065)


We pair session types and contracts using two encodings. The encoding of session types accommodates width and depth subtyping, two properties that partially hold in contracts. The encoding of contracts accommodates complex synchronization patterns, since session types own a simple control protocol. The encodings allow one to use the two formalisms interchangeably, within the context of dyadic interactions.


Normal Form Deductive System Service Contract Dyadic Interaction Syntax Tree 
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.
    Asperti, A., Laneve, C.: Interaction systems I: The theory of optimal reductions. Mathematical Structures in Computer Science 4(4), 457–504 (1994)zbMATHMathSciNetCrossRefGoogle Scholar
  2. 2.
    Boreale, M., De Nicola, R., Pugliese, R.: Basic observables for processes. Information and Computation 149(1), 77–98 (1999)zbMATHCrossRefMathSciNetGoogle Scholar
  3. 3.
    Carpineti, S., Castagna, G., Laneve, C., Padovani, L.: A formal account of contracts for Web Services. In: Bravetti, M., Núñez, M., Zavattaro, G. (eds.) WS-FM 2006. LNCS, vol. 4184, pp. 148–162. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  4. 4.
    Castagna, G., Gesbert, N., Padovani, L.: A theory of contracts for web services. In: POPL 2008: Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pp. 261–272. ACM, New York (2008)CrossRefGoogle Scholar
  5. 5.
    Cleaveland, R., Hennessy, M.: Testing equivalence as a bisimulation equivalence. Formal Aspects of Computing 5(1), 1–20 (1993)zbMATHCrossRefGoogle Scholar
  6. 6.
    De Nicola, R.: Two complete axiom systems for a theory of communicating sequential processes. Information and Control 64(1–3), 136–172 (1985)zbMATHCrossRefMathSciNetGoogle Scholar
  7. 7.
    De Nicola, R., Hennessy, M.: Testing equivalences for processes. Theoretical Computer Science 34, 83–133 (1984)zbMATHCrossRefMathSciNetGoogle Scholar
  8. 8.
    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
  9. 9.
    Dezani-Ciancaglini, M., de’ Liguoro, U., Yoshida, N.: On Progress for Structured Communications. In: Barthe, G., Fournet, C. (eds.) TGC 2007. LNCS, vol. 4912, pp. 257–275. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  10. 10.
    Dezani-Ciancaglini, M., Mostrous, D., Yoshida, N., Drossopoulou, S.: Session Types for Object-Oriented Languages. In: Thomas, D. (ed.) ECOOP 2006. LNCS, vol. 4067, pp. 328–352. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  11. 11.
    Gay, S., Hole, M.: Subtyping for session types in the π-calculus. Acta Informatica 42(2-3), 191–225 (2005)zbMATHCrossRefMathSciNetGoogle Scholar
  12. 12.
    Hennessy, M.: Acceptance trees. JACM: Journal of the ACM 32(4), 896–928 (1985)zbMATHMathSciNetGoogle Scholar
  13. 13.
    Hennessy, M.: Algebraic Theory of Processes. Foundation of Computing. MIT Press, Cambridge (1988)zbMATHGoogle Scholar
  14. 14.
    Honda, K.: Types for dyadic interaction. In: Best, E. (ed.) CONCUR 1993. LNCS, vol. 715, pp. 509–523. Springer, Heidelberg (1993)Google Scholar
  15. 15.
    Laneve, C., Padovani, L.: The must preorder revisited – an algebraic theory for web services contracts. In: Caires, L., Vasconcelos, V.T. (eds.) CONCUR. LNCS, vol. 4703, pp. 212–225. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  16. 16.
    Vasconcelos, V., Gay, S., Ravara, A.: Type checking a multithreaded functional language with session types. Theoretical Computer Science 368 (2006)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2008

Authors and Affiliations

  • Cosimo Laneve
    • 1
  • Luca Padovani
    • 2
  1. 1.Department of Computer ScienceUniversity of Bologna 
  2. 2.Information Science and Technology InstituteUniversity of Urbino 

Personalised recommendations