A Convex Powerdomain over Lattices: its Logic and λ-Calculus

Abstract

To model at the same time parallel and nondeterministic functional calculi we define a powerdomain functor Ρ such that it is an endofunctor over the category of algebraic lattices. Ρ is locally continuous and we study the initial solution D^∞ of the domain equation D = Ρ([D → D]_⊥). We derive from the algebras of Ρ the logic of D^∞, that is the axiomatic description of its compact elements. We then define a λ-calculus and a type assignment system using the logic of D^∞ as the related type theory. We prove that the filter model of this calculus, which is isomorphic to D^∞, is fully abstract with respect to the observational Preorder of the λ-calculus.