Typechecking safe process synchronization

Título:

Typechecking safe process synchronization

Autor:

Bonelli, Eduardo

Colaboradores:

; Compagnoni, Adriana; Gunter, Elsa L.

Temas:

PROGRAMACIÓN CONCURRENTECOMUNICACIÓN ENTRE PROCESOSCÁLCULO PI

En:

Electronic Notes in Theoretical Computer Science Vol 138 No. 1 pp. 3-22, 2004. Proceedings of the Workshop on the Foundations of Global Ubiquitous Computing (FGUC 2004)

Resumen:

Session types describe the interactions between two parties within multi-party communications. They constitute a communication protocol in the sense that the order and type of interactions between two parties are specified. For their part, correspondence assertions provide a mechanism for synchronization. When session types and correspondence assertions are combined, they are able to describe synchronization across different communication sessions, yielding a rich language for imposing expressive interaction patterns in multi-party communications. This paper studies the typechecking problem for Iris, a typed π-calculus that combines session types and correspondence assertions. We define a typechecking algorithm and prove that it is sound and complete with respect to the typing rules. Furthermore, we show that the typing system satisfies the minimum effects property. Although session types have been extensively studied in the past few years, to our knowledge this is the first proof of decidability of typechecking for a type system with session types. -- Keywords: Concurrency; π-calculus; type systems; typechecking.

URL/DOI:

Medio:

Soporte electrónico

Tipo de documento:

Artículo

Idioma:

Inglés

Publicación:

, 2004

Puede solicitar más fácilmente el ejemplar con: A0189

Ver estantes