FILTER MODELS FOR CONJUNCTIVE-DISJUNCTIVE LAMBDA-CALCULI

The distinction between the conjunctive nature of non-determinism as o pposed to the disjunctive character of parallelism constitutes the mot ivation and the starting point of the present work. lambda-calculus is extended with both a non-deterministic choice and a parallel operator ; a notion of reduction is introduced, extending beta-reduction of the classical calculus. We study type assignment systems for this calculu s, together with a denotational semantics which is initially defined c onstructing a set semimodel via simple types. We enrich the type syste m with intersection and union types, dually reflecting the disjunctive and conjunctive behaviour of the operators, and we build a filter mod el. The theory of this model is compared both with a Morris-style oper ational semantics and with a semantics based on a notion of capabiliti es.