Skip to Main content Skip to Navigation
Reports

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 :
Reports
Complete list of metadata

Cited literature [16 references]  Display  Hide  Download

https://hal.inria.fr/inria-00424248
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

File

RR-7063.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : inria-00424248, version 1

Citation

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

Share

Metrics

Record views

257

Files downloads

122