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

Cited literature [16 references]  Display  Hide  Download

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

File

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

Identifiers

  • HAL Id : inria-00424248, version 1

Collections

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

528

Files downloads

215