The Coq mailing list

[Robert <robdockins AT fastmail.fm>]

I don't know how suitable my domain theory development is for didactic 
purposes, but I'll say that the last time I looked (which was admittedly 
several years ago) my development was the most complete Coq development 
of domain theory in terms of the sophistocation of the concepts 
covered.  I set out to create an "industrial strength" development that 
could be used for realistic semantic arguments, and which was also fully 
constructive.  In that, I think I succeeded.  My development doesn't 
quite follow a textbook presentation, but I'm not convinced that any 
axiom-free Coq development of domain theory could.

As a brief description, I succeded in deveoping a constructive theory of 
bifinite domains suitable for denotational semantics of untyped and 
typed languages, which admits all the usual constructions (products, 
sums, function spaces, recursive functions), as well as more advanced 
constructions, including recursive solutions of domain equations (via 
fixpoints of continuous functors in the ep-pair category), and the 
typical powerdomains (upper, lower, and convex).  As a proof-of-concept, 
I've carried out soundness and adequacy (equal denotations implies 
contextual equivance) proofs for a small collection of simple combinator 
and labmda-based calculi.

I don't have much time these days to work on this stuff, but I'm happy 
to answer questions and such, if that's helpful.

Cheers,
  Rob


On 01/05/2018 01:08 PM, Benjamin C. Pierce wrote:
> I’m looking for a nice development of “textbook domain theory” in Coq, to 
> supplement some lectures in a graduate course.  Google pointed me to ones by 
> Rob Dawkins and Nick Benton, but I’m sure there must be lots of others.  Any 
> particular recommendations?
>
> Thanks!
>
>      - Benjamin