14th Annual IEEE Symposium on Logic in Computer Science (LICS'99)
Cartesian Closed Double Categories, Their Lambda-Notation, and the Pi-Calculus
Trento, Italy
July 02-July 05
ISBN: 0-7695-0158-3
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