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.
A filter model for concurrent lambda-calculus / M., Dezani Ciancaglini; U., De'Liguoro; Piperno, Adolfo. - In: SIAM JOURNAL ON COMPUTING. - ISSN 0097-5397. - 27:(1998), pp. 1376-1419. [10.1137/s0097539794275860]
A filter model for concurrent lambda-calculus
PIPERNO, Adolfo
1998
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 abstract.File allegati a questo prodotto
Non ci sono file associati a questo prodotto.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
