A Coq library for domain theory


This library implements the theory of profinite and pointed profinite domains in Coq. All proofs and constructions are entirely constructive; in particular, no axioms beyond Coq's base metatheory are asserted.

All the standard domain constructions are provided including: products, sums, functions, lifting and powerdomains. In addition, recursive domain equations can be solved over continuous functors in these domains. Continuous functors are provided for all the standard constructions.

Several worked examples are provided, proving soundness and adequacy for several different systems:

Note: this proof development makes heavy used of UTF mathematical symbols. Depending on your system configuration, you might need to install additional font support for such symbols to view the source and documentation.

Quick links