We present a type theory for analyzing concurrent multiparty interactions as found in service-oriented computing. Our theory introduces a novel and flexible type structure, able to uniformly describe both the internal and the interface behavior of systems, referred respectively as choreographies and contracts in web-services terminology. The notion of conversation builds on the fundamental concept of session, but generalizes it along directions up to now unexplored; in particular, conversation types discipline interactions in conversations while accounting for dynamical join and leave of an unanticipated number of participants. We prove that well-typed systems never violate the prescribed conversation constraints. We also present techniques to ensure progress of systems involving several interleaved conversations, a previously open problem.
|Title of host publication||Lecture Notes in Computer Science, Springer-Verlag|
|Publication status||Published - 1 Jan 2009|
|Event||Programming Languages and Systems, 18th European Symposium on Programming (ESOP) - |
Duration: 1 Jan 2009 → …
|Conference||Programming Languages and Systems, 18th European Symposium on Programming (ESOP)|
|Period||1/01/09 → …|