Paper: Strong Normalisation in the π-Calculus (at LICS 2001)

Authors: Kohei Honda Nobuko Yoshida Martin Berger

Abstract

Introduces a typed π-calculus where strong normalisation is ensured by typability. Strong normalisation is a useful property in many computational contexts, including distributed systems. In spite of its simplicity, our type discipline captures a wide class of converging name-passing interactive behaviours. The proof of strong normalisability combines methods from typed λ-calculi and linear logic with process-theoretic reasoning. It is adaptable to systems involving state and other extensions. Strong normalisation is shown to have significant consequences, including finite axiomatisation of weak bisimilarity, a fully abstract embedding of the simply-typed λ-calculus with products and sums and basic liveness in interaction. Strong normalisability has been extensively studied as a fundamental property in functional calculi, term rewriting and logical systems. This work is one of the first steps to extend theories and proof methods for strong normalisability to the context of name-passing processes

BibTeX

  @InProceedings{HondaYoshidaBerger-StrongNormalisation,
    author = 	 {Kohei Honda and Nobuko Yoshida and Martin Berger},
    title = 	 {Strong Normalisation in the π-Calculus},
    booktitle =  {Proceedings of the Sixteenth Annual IEEE Symposium on Logic in Computer Science (LICS 2001)},
    year =	 {2001},
    month =	 {June}, 
    pages =      {311--322},
    location =   {Boston, MA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }