# Logic in Computer Science (LICS 1995)

## Paper: Modal µ-Types for Processes (at LICS 1995)

### Abstract

We introduce a new paradigm for concurrency, called behaviors-as- types. In this paradigm, types are used to convey information about the behavior of processes: while terms corresponds to processes, types correspond to behaviors. We apply this paradigm to Winskel's Process Algebra. Its types are similar to Kozen's modal \mu-calculus; hence, they are called modal \mu-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.

### BibTeX

  @InProceedings{MiculanGadducci-ModalTypesforProces,
author = 	 {Marino Miculan and Fabio Gadducci},
title = 	 {Modal µ-Types for Processes},
booktitle =  {Proceedings of the Tenth Annual IEEE Symp. on Logic in Computer Science, {LICS} 1995},
year =	 1995,
editor =	 {Dexter Kozen},
month =	 {June},
pages =      {221-231},
location =   {San Diego, CA, USA},
publisher =	 {IEEE Computer Society Press}
}