We define a powerdomain functor over algebraic lattices to model parallel and non deterministic lambda-calculi. We derive a logic and a type system for such a calculus and obtain a filter-model which is fully abstract w.r.t. the observational preorder.
A Convex Powerdomain over Lattices: its Logic and λ-Calculus
DEZANI, Mariangiola;DE' LIGUORO, Ugo
1997-01-01
Abstract
We define a powerdomain functor over algebraic lattices to model parallel and non deterministic lambda-calculi. We derive a logic and a type system for such a calculus and obtain a filter-model which is fully abstract w.r.t. the observational preorder.
File in 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.
