A Filter Model for Concurrent $\lambda$-Calculus
Mariangiola Dezani-Ciancaglini, Ugo de’Liguoro, Adolfo Piperno · SIAM Journal on Computing · 1998
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.