Lics

IEEE Symposium on Logic in Computer Science

LICS Home - LICS Awards - LICS Newsletters - LICS Archive - LICS Organization - Logic-Related Conferences - Links

Eighth Annual IEEE Symposium on

Logic in Computer Science (LICS 1993)

Paper: Typing and subtyping for mobile processes (at LICS 1993)

Winner of the Test-of-Time Award in 2013
Authors: Benjamin C. Pierce Davide Sangiorgi

Abstract

The π-calculus is a process algebra that supports process mobility by focusing on the communication of channels. R. Milner's (1991) presentation of the π-calculus includes a type system assigning arities to channels and enforcing a corresponding discipline in their use. The authors extend Milner's language of types by distinguishing between the ability to read from a channel, the ability to write to a channel, and the ability both to read and to write. This refinement gives rise to a natural subtype relation similar to those studied in typed λ-calculi. The greater precision of their type discipline yields stronger versions of some standard theorems about the π-calculus. These can be used, for example, to obtain the validity of β-reduction for the more efficient of Milner's encodings of the call-by-value λ-calculus, for which β-reduction does not hold in the ordinary π-calculus. The authors define the syntax, typing, subtyping, and operational semantics of their calculus, prove that the typing rules are sound, apply the system to Milner's λ-calculus encodings, and sketch extensions to higher-order process calculi and polymorphic typing

BibTeX

  @InProceedings{PierceSangiorgi-Typingandsubtypingf,
    author = 	 {Benjamin C. Pierce and Davide Sangiorgi},
    title = 	 {Typing and subtyping for mobile processes},
    booktitle =  {Proceedings of the Eighth Annual IEEE Symposium on Logic in Computer Science (LICS 1993)},
    year =	 {1993},
    month =	 {June}, 
    pages =      {376--385},
    location =   {Montreal, Canada}, 
    publisher =	 {IEEE Computer Society Press}
  }
   

Last modified: 2016-01-1416:21
Andrzej Murawski