Skip to Main content Skip to Navigation

A Categorical Semantics for The Parallel Lambda-Calculus

Germain Faure 1, 2 Alexandre Miquel 3 
2 TYPICAL - Types, Logic and computing
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France
Abstract : In this report, we define a sound and complete categorical semantics for the parallel lambda-calculus, based on a notion of 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 some model. We also 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, and check that G. Boudol's original semantics is a particular case of ours.
Document type :
Complete list of metadata

Cited literature [16 references]  Display  Hide  Download
Contributor : Germain Faure Connect in order to contact the contributor
Submitted on : Wednesday, October 14, 2009 - 3:51:27 PM
Last modification on : Friday, February 4, 2022 - 3:13:42 AM
Long-term archiving on: : Tuesday, October 16, 2012 - 12:15:30 PM


Files produced by the author(s)


  • HAL Id : inria-00424248, version 1


Germain Faure, Alexandre Miquel. A Categorical Semantics for The Parallel Lambda-Calculus. [Research Report] RR-7063, INRIA. 2009, pp.22. ⟨inria-00424248⟩



Record views


Files downloads