Logic in Computer Science (LICS 2005)

Paper: Semantic Subtyping for the p-Calculus (at LICS 2005)

Authors: Giuseppe Castagna Rocco De Nicola Daniele Varacca

Abstract

Subtyping relations for the p-calculus are usually de- fined in a syntactic way, by means of structural rules. We propose a semantic characterisation of channel types and use it to derive a subtyping relation. The type system we consider includes read-only and write-only channel types, as well as boolean combinations of types. A set-theoretic interpretation of types is provided, in which boolean combinations are interpreted as the corresponding set-theoretic operations. Subtyping is defined as inclusion of the interpretations. We prove the decidability of the subtyping relation and sketch the subtyping algorithm. In order to fully exploit the type system, we define a variant of the p-calculus where communication is subjected to pattern matching that performs dynamic typecase.

BibTeX

  @InProceedings{CastagnaDeNicolaVar-SemanticSubtypingfo,
    author = 	 {Giuseppe Castagna and Rocco De Nicola and Daniele Varacca},
    title = 	 {Semantic Subtyping for the p-Calculus},
    booktitle =  {Proceedings of the Twentieth Annual IEEE Symp. on Logic in Computer Science, {LICS} 2005},
    year =	 2005,
    editor =	 {Prakash Panangaden},
    month =	 {June}, 
    pages =      {92--101},
    location =   {Chicago, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }