15/02/2007
Germain Faure (LORIA)
A Categorical Semantics for The Parallel Lambda-Calculus

In the first part of this talk, I present what the starting point of this work was: a denotational semantics for the rho-calculus (a.k.a. the rewriting calculus) of Cirstea and Kirchner. Then, I explain why we switch to the study of the parallel lambda-calculus, pointing out some similarities between both calculus and some interesting problems related to the interactions between pattern-matching and parallelism.

In the second part, I define a sound and complete categorical semantics for the parallel lambda-calculus, based on a notion on aggregation monad which is modular w.r.t. associativity, commutativity and idempotence. To prove completeness, we introduce a category of partial equivalence relations adapted to parallelism, in which any extension of the basic equational theory of the calculus is induced by a particular model.

In the third part, I present abstract methods to construct models of the parallel lambda-calculus in categories where particular equations have solutions, such as the category of Scott domains and its variants. In particular, we show that G. Boudol's original semantics is a particular case of ours.

This is a joint work with Alexandre Miquel.