Correspondence assertions for process synchronization in concurrent communications

High-level specification of patterns of communications such as protocols can be modeled elegantly by means of session types. However, a number of examples suggest that session types fall short when finer precision on protocol specification is required. In order to increase the expressiveness of sess...

Descripción completa

Guardado en:

Detalles Bibliográficos
Autores principales:	Bonelli, Eduardo, Compagnoni, Adriana, Gunter, Elsa
Formato:	Articulo
Lenguaje:	Inglés
Publicado:	2004
Materias:	Ciencias Informáticas Concurrent programming Correspondence assertions Pi-calculus Session types Type systems
Acceso en línea:	http://sedici.unlp.edu.ar/handle/10915/84912
Aporte de:	SEDICI (UNLP) de Universidad Nacional de La Plata

id	I19-R120-10915-84912
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 Concurrent programming Correspondence assertions Pi-calculus Session types Type systems
spellingShingle	Ciencias Informáticas Concurrent programming Correspondence assertions Pi-calculus Session types Type systems Bonelli, Eduardo Compagnoni, Adriana Gunter, Elsa Correspondence assertions for process synchronization in concurrent communications
topic_facet	Ciencias Informáticas Concurrent programming Correspondence assertions Pi-calculus Session types Type systems
description	High-level specification of patterns of communications such as protocols can be modeled elegantly by means of session types. However, a number of examples suggest that session types fall short when finer precision on protocol specification is required. In order to increase the expressiveness of session types we appeal to the theory of correspondence assertions. The resulting type discipline augments the types of long term channels with effects and thus yields types which may depend on messages read or written earlier within the same session. We prove that evaluation preserves typability and that well-typed processes are safe. Also, we illustrate how the resulting theory allows us to address the shortcomings present in the pure theory of 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	Correspondence assertions for process synchronization in concurrent communications
title_short	Correspondence assertions for process synchronization in concurrent communications
title_full	Correspondence assertions for process synchronization in concurrent communications
title_fullStr	Correspondence assertions for process synchronization in concurrent communications
title_full_unstemmed	Correspondence assertions for process synchronization in concurrent communications
title_sort	correspondence assertions for process synchronization in concurrent communications
publishDate	2004
url	http://sedici.unlp.edu.ar/handle/10915/84912
work_keys_str_mv	AT bonellieduardo correspondenceassertionsforprocesssynchronizationinconcurrentcommunications AT compagnoniadriana correspondenceassertionsforprocesssynchronizationinconcurrentcommunications AT gunterelsa correspondenceassertionsforprocesssynchronizationinconcurrentcommunications
bdutipo_str	Repositorios
_version_	1764820488703442949

Correspondence assertions for process synchronization in concurrent communications

Ejemplares similares