| pcd06 (In proceedings)
|
| Author(s) | Pablo Garralda, Adriana Compagnoni and Mariangiola Dezani-Ciancaglini |
| Title | « BASS: Boxed Ambients with Safe Sessions » |
| In | PPDP'06 |
| Editor(s) | Michael Maher |
| Page(s) | 61-72 |
| Year | 2006 |
| Publisher | ACM Press |
| PDF | http://www.di.unito.it/˜dezani/papers/bass.pdf |
| Abstract |
| We define BASS, a typed boxed ambients calculus with safe sessions. Sessions offer the possibility of using the same channel to transmit information of different types in a prescribed order. A session involves two communicating processes located either within the same ambient or across an ambient boundary. One of the challenges of adding session primitives to a mobile calculus is how to protect sessions from being interrupted by a mobility step. To address this challenge, we introduce a mechanism that prevents an ambient from moving, if there are pending sessions across its boundary. The main result of our development is that in a well-typed process a communication redex never disappears after a mobility step. In other words, the residual of a communication redex is present in the reduct of the original process enabling a pending session step to be completed. Therefore, we say that sessions in our calculus are safe. |
@inproceedings{pcd06,
pdf = {http://www.di.unito.it/~dezani/papers/bass.pdf},
author = {Pablo Garralda and Adriana Compagnoni and Mariangiola
Dezani-Ciancaglini},
booktitle = {{PPDP'06}},
editor = {Michael Maher},
title = {{BASS: Boxed Ambients with Safe Sessions}},
abstract = { We define BASS, a typed boxed ambients calculus with safe
sessions. Sessions offer the possibility of using the same channel
to transmit information of different types in a prescribed order.
A session involves two communicating processes located either
within the same ambient or across an ambient boundary. One of the
challenges of adding session primitives to a mobile calculus is
how to protect sessions from being interrupted by a mobility step.
To address this challenge, we introduce a mechanism that prevents
an ambient from moving, if there are pending sessions across its
boundary. The main result of our development is that in a
well-typed process a communication redex never disappears after a
mobility step. In other words, the residual of a communication
redex is present in the reduct of the original process enabling a
pending session step to be completed. Therefore, we say that
sessions in our calculus are safe.},
publisher = {{ACM Press}},
pages = {61-72},
year = 2006,
}
This document was generated by bib2html 3.3.
(Modified by Luca Paolini, under the GNU General Public License)
