We study two refinements of the linear π-calculus that ensure deadlock freedom (the absence of stable states with pending linear communications) and lock freedom (the eventual completion of pending linear communications). The main feature of both type systems is a new form of channel polymorphism that affects their accuracy in a significant way: they are the first of their kind that can deal with recursive processes connected by cyclic networks.
Deadlock and Lock Freedom in the Linear π-Calculus
PADOVANI, Luca
2014-01-01
Abstract
We study two refinements of the linear π-calculus that ensure deadlock freedom (the absence of stable states with pending linear communications) and lock freedom (the eventual completion of pending linear communications). The main feature of both type systems is a new form of channel polymorphism that affects their accuracy in a significant way: they are the first of their kind that can deal with recursive processes connected by cyclic networks.
File in questo prodotto:
| File | Dimensione | Formato | |
|---|---|---|---|
|
lics_2014.pdf
Accesso aperto
Tipo di file:
POSTPRINT (VERSIONE FINALE DELL’AUTORE)
Dimensione
378 kB
Formato
Adobe PDF
|
378 kB | Adobe PDF | Visualizza/Apri |
|
2014 - LICS - Padovani - Deadlock and lock freedom in the linear pi-calculus.pdf
Accesso riservato
Tipo di file:
PDF EDITORIALE
Dimensione
592.7 kB
Formato
Adobe PDF
|
592.7 kB | Adobe PDF | Visualizza/Apri Richiedi una copia |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
