Formalized, effective domain theory in Coq

ABSTRACT. I present highlights from a formalized development of do- main theory in the theorem prover Coq. This is the first development of domain theory that is effective, formalized and that supports all the usual constructions on domains. In particular, I develop constructive models of both the unpointed profinite and the pointed profinite domains. tandard constructions (e.g., products, sums, the function space, and powerdomains) are all developed. In addition, I build the machinery necessary to compute solutions to recursive domain equations.