The distinction between the conjunctive nature of non-determinism as opposed to the disjunctive character of parallelism constitutes the motivation and the starting point of the present work. λ-calculus is extended with both a non-deterministic choice and a parallel operator; a notion of reduction is introduced, extending β-reduction of the classical calculus. We study type assignment systems for this calculus, together with a denotational semantics which is initially defined constructing a set semimodel via simple types. We enrich the type system with intersection and union types, dually reflecting the disjunctive and conjunctive behaviour of the operators, and we build a filter model. The theory of this model is compared both with a Morris-style operational semantics and with a semantics based on a notion of capabilities.
Dezani-Ciancaglini, M., de’Liguoro, U., & Piperno, A. (1996). Filter models for conjunctive-disjunctive λ-calculi. Theoretical Computer Science, 170(1–2), 83–128. https://doi.org/10.1016/S0304-3975(96)00235-6