Lambda-Calculi for (Strict) Parallel Functions

We introduce two λ-calculi and show that they are expressive for two canonical domains of parallel functions. The first calculus is an enrichment of the lazy, call-by-name λ-calculus with call-by-value abstractions and parallel composition, while in the second the usual call-by-name abstractions are disallowed. The corresponding domains are respectively Abramsky′s domain D = (D →⊥ D)⊥, a lifted function space, and D = (D →⊥ D)⊥, a lifted domain of strict functions. These domains are lattices, and we show that the parallelism is adequately represented by the join operator, while call-by-value abstractions correspond to strict functions. The proofs of the results rely on a completeness theorem for the logical presentation of the semantics.

Authors

• G. Boudol

Keywords

No keywords are indexed for this paper.