loading...
Cartesian Closed Double Categories, Their Lambda-Notation, and the Pi-Calculus
Trento, Italy July 02-July 05
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/LICS.1999.78262014th Annual IEEE Symposium on Logic i ...
 This Article 
 
PDF
HTML
 
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Roberto Bruni, University of Pisa
Ugo Montanari, University of Pisa
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.
Index Terms:
cartesian closed categories, lambda-calculus, double categories, pi-calculus, mobile calculi, higher-order communications
Citation:
Roberto Bruni, Ugo Montanari, "Cartesian Closed Double Categories, Their Lambda-Notation, and the Pi-Calculus," lics, pp.246, 14th Annual IEEE Symposium on Logic in Computer Science (LICS'99), 1999
Usage of this product signifies your acceptance of the Terms of Use.