A carregar...
Publicação
A universal session type for untyped asynchronous communication
| Nome: | Descrição: | Tamanho: | Formato: | |
|---|---|---|---|---|
| 661.49 KB | Adobe PDF |
Orientador(es)
Resumo(s)
In the simply-typed λ-calculus we can recover the full range of expressiveness of the untyped λ-calculus solely by adding a single recursive type U = U → U. In contrast, in the session-typed π-calculus, recursion alone is insu cient to recover the untyped π-calculus, primarily due to linearity: each channel just has two unique endpoints. In this paper, we show that shared channels with a corresponding sharing semantics (based on the language SILLS developed in prior work) are enough to embed the untyped asynchronous π-calculus via a universal shared session type US. We show that our encoding of the asynchronous π-calculus satisfies operational correspondence and preserves observable actions (i.e., processes are weakly bisimilar to their encoding). Moreover, we clarify the expressiveness of SILLS by developing an operationally correct encoding of SILLS in the asynchronous π-calculus.
Descrição
Palavras-chave
Bisimulation Phrases session types Sharing Π-calculus Software
Contexto Educativo
Citação
Editora
Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing