Invited Paper: Cartesian Closed Double Categories, Their Lambda-Notation, and the Pi-Calculus (at LICS 1999)

Authors: Roberto Bruni Ugo Montanari

Abstract

We introduce the notion of cartesian closed double category to provide mobile calculi for communicating systems with specific semantic models: One dimension is dedicated to compose systems and the other to compose their computations and their observations. Also, inspired by the connection between simply typed lambda-calculus and cartesian closed categories, we define a new typed framework, called double lambda-notation, which is able to express the abstraction/application and pairing/projection operations in all dimensions. In this development, we take the categorical presentation as a guidance in the interpretation of the formalism. A case study of the pi-calculus, where the double lambda-notation straightforwardly handles name passing and creation, concludes the presentation.

BibTeX

  @InProceedings{BruniMontanari-CartesianClosedDoub,
    author = 	 {Roberto Bruni and Ugo Montanari},
    title = 	 {Cartesian Closed Double Categories, Their Lambda-Notation, and the Pi-Calculus},
    booktitle =  {Proceedings of the Fourteenth Annual IEEE Symposium on Logic in Computer Science (LICS 1999)},
    year =	 {1999},
    month =	 {July}, 
    pages =      {246--265},
    location =   {Trento, Italy}, 
    note =       {Invited Talk},
    publisher =	 {IEEE Computer Society Press}
  }