The essence of parallel Algol

We consider a parallel Algol-like language, combining the λ-calculus with shared-variable parallelism. We provide a denotational semantics for this language, simultaneously adapting the possible worlds model of Reynolds and Oles (1981, 1982) to the parallel setting and generalizing the “transition traces” model to the procedural setting. This semantics supports reasoning about safety and liveness properties of parallel programs, and validates a number of natural laws of program equivalence based on noninterference properties of local variables. We also provide a relationally parametric semantics, to permit reasoning about relation-preserving properties of programs, and adapting work of O´Hearn and Tennent (1995) to the parallel setting. This semantics supports standard methods of reasoning about representational independence. The clean design of the programming language and its semantics supports the orthogonality of procedures and shared-variable parallelism