The fusion calculi are a simplification of the pi-calculus in which input and output are symmetric and restriction is the only binder. We highlight a major difference between these calculi and the pi-calculus from the point of view of types, proving some impossibility results for subtyping in fusion calculi. We propose a modification of fusion calculi in which the name equivalences produced by fusions are replaced by name preorders, and with a distinction between positive and negative occurrences of names. The resulting calculus allows us to import subtype systems, and related results, from the pi-calculus. We examine the consequences of the modification on behavioural equivalence (e.g., context-free characterisations of barbed congruence) and expressiveness (e.g., full abstraction of the embedding of the asynchronous pi-calculus).
Name-passing calculi: From fusions to preorders and types / Hirschkoff, Daniel; Madiot, Jean-Marie; Sangiorgi, Davide. - In: INFORMATION AND COMPUTATION. - ISSN 0890-5401. - STAMPA. - 251:(2016), pp. 335-360. [10.1016/j.ic.2016.10.003]
Name-passing calculi: From fusions to preorders and types
MADIOT, JEAN MARIE;SANGIORGI, DAVIDE
2016
Abstract
The fusion calculi are a simplification of the pi-calculus in which input and output are symmetric and restriction is the only binder. We highlight a major difference between these calculi and the pi-calculus from the point of view of types, proving some impossibility results for subtyping in fusion calculi. We propose a modification of fusion calculi in which the name equivalences produced by fusions are replaced by name preorders, and with a distinction between positive and negative occurrences of names. The resulting calculus allows us to import subtype systems, and related results, from the pi-calculus. We examine the consequences of the modification on behavioural equivalence (e.g., context-free characterisations of barbed congruence) and expressiveness (e.g., full abstraction of the embedding of the asynchronous pi-calculus).I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.