A Filter Model for Concurrent $\lambda$-Calculus

Abstract

Type-free lazy $\lambda$-calculus is enriched with angelic parallelism and demonic nondeterminism. Call-by-name and call-by-value abstractions are considered and the operational semantics is stated in terms of a must convergence predicate. We introduce a type assignment system with intersection and union types, and we prove that the induced logical semantics is fully abstract.