A Filter Model for Concurrent $\lambda$-Calculus
- 1 October 1998
- journal article
- Published by Society for Industrial & Applied Mathematics (SIAM) in SIAM Journal on Computing
- Vol. 27 (5) , 1376-1419
- https://doi.org/10.1137/s0097539794275860
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 abstractKeywords
This publication has 33 references indexed in Scilit:
- Intersection type assignment systemsTheoretical Computer Science, 1995
- Intersection and Union Types: Syntax and SemanticsInformation and Computation, 1995
- A Semantics for Static Type Inference in a Nondeterministic LanguageInformation and Computation, 1994
- Full Abstraction in the Lazy Lambda CalculusInformation and Computation, 1993
- Complete restrictions of the intersection type disciplineTheoretical Computer Science, 1992
- Domain theory in logical form*Annals of Pure and Applied Logic, 1991
- Observation equivalence as a testing equivalenceTheoretical Computer Science, 1987
- Parametric channels via label expressions in CCSTheoretical Computer Science, 1984
- A mathematical semantics for a nondeterministic typed λ-calculusTheoretical Computer Science, 1980
- Nondeterminism and fully abstract modelsRAIRO. Informatique théorique, 1980