We introduce a new paradigm for concurrency, called behaviours-as-types. In this paradigm, types are used to convey information about the behaviour of processes: while terms corresponds to processes, types correspond to behaviours. We apply this paradigm to Winskel's Process Algebra. Its types are similar to Kozen's modal μ-calculus; hence, they are called modal μ-types. We prove that two terms having the same type denote two processes which behave in the same way, that is, they are bisimilar. We give a sound and complete compositional typing system for this language. Such a system naturally recovers the notion of bisimulation also on open terms, allowing us to deal with processes with undefined parts in a compositional manner.

Modal μ-types for processes

GADDUCCI, FABIO
1995-01-01

Abstract

We introduce a new paradigm for concurrency, called behaviours-as-types. In this paradigm, types are used to convey information about the behaviour of processes: while terms corresponds to processes, types correspond to behaviours. We apply this paradigm to Winskel's Process Algebra. Its types are similar to Kozen's modal μ-calculus; hence, they are called modal μ-types. We prove that two terms having the same type denote two processes which behave in the same way, that is, they are bisimilar. We give a sound and complete compositional typing system for this language. Such a system naturally recovers the notion of bisimulation also on open terms, allowing us to deal with processes with undefined parts in a compositional manner.
1995
0818670509
File in questo prodotto:
Non ci sono file associati a questo prodotto.

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/11568/26910
 Attenzione

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

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