Filter models for conjunctive-disjunctive λ-calculi

Citations of this article
Mendeley users who have this article in their library.
Get full text


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.

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free