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
Inria Saclay - Ile de France, LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau]
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 <>
Submitted on : Wednesday, October 14, 2009 - 3:51:27 PM
Last modification on : Friday, March 27, 2020 - 3:49:54 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