We introduce an interpretation of domains in terms of a logic including bounded existential and universal quantifiers. The logic is compositional with respect to domain constructors like function space and Plotkin powerdomain, and sound with respect to the ordinary interpreation of domains as some kind of complete partial orders. A major fragment of this logic is also proved complete.

A first order modal logic, Hoare logic for partial and total correctness, as well as second order polymorphic lambda calculus with subtypes can be seen as special instances of FOLD.