Modelling higher-order dual nondeterminacy

We investigate models for programming and specifying in which higher-order functions and nondeterminacy (both demonic and angelic) coexist. The models are built using predicate transformers, binary multirelations, state transformers, and free lattices over a poset. We show there exist suitable models in each approach, and that they are isomorphic. The models support an algebra of nondeterminacy which we use to prove that the classical list fusion law holds even in the presence of nondeterminacy.