Typechecking safe process synchronization

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 synchroniz...

Descripción completa

Guardado en:
Detalles Bibliográficos
Autores principales: Bonelli, Eduardo, Compagnoni, Adriana, Gunter, Elsa
Formato: Articulo
Lenguaje:Inglés
Publicado: 2005
Materias:
Ciencias Informáticas
π-calculus
Concurrency
Type systems
Typechecking
Acceso en línea:http://sedici.unlp.edu.ar/handle/10915/83379
Aporte de:
SEDICI (UNLP) de Universidad Nacional de La Plata
id I19-R120-10915-83379
record_format dspace
institution Universidad Nacional de La Plata
institution_str I-19
repository_str R-120
collection SEDICI (UNLP)
language Inglés
topic Ciencias Informáticas
π-calculus
Concurrency
Type systems
Typechecking
spellingShingle Ciencias Informáticas
π-calculus
Concurrency
Type systems
Typechecking
Bonelli, Eduardo
Compagnoni, Adriana
Gunter, Elsa
Typechecking safe process synchronization
topic_facet Ciencias Informáticas
π-calculus
Concurrency
Type systems
Typechecking
description 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.
format Articulo
Articulo
author Bonelli, Eduardo
Compagnoni, Adriana
Gunter, Elsa
author_facet Bonelli, Eduardo
Compagnoni, Adriana
Gunter, Elsa
author_sort Bonelli, Eduardo
title Typechecking safe process synchronization
title_short Typechecking safe process synchronization
title_full Typechecking safe process synchronization
title_fullStr Typechecking safe process synchronization
title_full_unstemmed Typechecking safe process synchronization
title_sort typechecking safe process synchronization
publishDate 2005
url http://sedici.unlp.edu.ar/handle/10915/83379
work_keys_str_mv AT bonellieduardo typecheckingsafeprocesssynchronization
AT compagnoniadriana typecheckingsafeprocesssynchronization
AT gunterelsa typecheckingsafeprocesssynchronization
bdutipo_str Repositorios
_version_ 1764820488556642304

Ejemplares similares