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:

- simply-typed SKI calculus with booleans
- simply-typed SKI calculus with booleans and fixpoints
- simply-typed lambda-calculus with booleans
- simply-typed lambda-calculus with booleans and fixpoints

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.

- Download proof source
- Source repository
- Source-level documentation
- An overview paper, explaining the high-level ideas