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 sub typing 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 Types2013 28th Annual ACM/IEEE Symposium on Logic in Computer Science / Daniel Hirschkoff;Jean-Marie Madiot;Davide Sangiorgi. - STAMPA. - (2013), pp. 378-387. (Intervento presentato al convegno 28TH ANNUAL IEEE/ACM SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE tenutosi a New Orleans, USA nel Giugno 25-28, 2013) [10.1109/LICS.2013.44].

Name-Passing Calculi: From Fusions to Preorders and Types2013 28th Annual ACM/IEEE Symposium on Logic in Computer Science

SANGIORGI, DAVIDE
2013

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 sub typing 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).
2013
28th Annual ACM/IEEE Symposium on Logic in Computer Science
378
387
Name-Passing Calculi: From Fusions to Preorders and Types2013 28th Annual ACM/IEEE Symposium on Logic in Computer Science / Daniel Hirschkoff;Jean-Marie Madiot;Davide Sangiorgi. - STAMPA. - (2013), pp. 378-387. (Intervento presentato al convegno 28TH ANNUAL IEEE/ACM SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE tenutosi a New Orleans, USA nel Giugno 25-28, 2013) [10.1109/LICS.2013.44].
Daniel Hirschkoff;Jean-Marie Madiot;Davide Sangiorgi
File in questo prodotto:
Eventuali allegati, non sono esposti

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11585/378843
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 8
  • ???jsp.display-item.citation.isi??? 8
social impact