Powerdomains and nondeterminism in synthetic domain theory
Provides a foundational framework for nondeterminism in synthetic domain theory, benefiting researchers in semantics and type theory.
The paper constructs lower, upper, and convex powerdomains in synthetic domain theory and proves they yield computationally adequate denotational models of nondeterminism, enabling a nondeterministic metalanguage embedded in dependent type theory for reasoning about program behavior.
Synthetic domain theory is an axiomatization of domain theory within a constructive universe of sets such that all definable maps between domains are continuous. In this paper we construct the counterparts to the well-known lower, upper, and convex powerdomains in the setting of synthetic domain theory and prove that they produce computationally adequate denotational models of nondeterminism. By developing the theory of powerdomains in synthetic domain theory, we obtain a nondeterministic metalanguage that directly embeds into dependent type theory, where the latter serves as an expressive logic for reasoning about the metalanguage. Moreover, the computational adequacy results imply that denotational reasoning through the metalanguage may be used to study operational behaviors of actual programs.