[Agda] Domain Theory Libraries for Agda?

[Bas Spitters]

Perhaps not precisely what you are looking for, but there is some
domain theory in Coq.

This paper has been accepted for ITP'14.
Robert Dockins. Formalized, effective domain theory in Coq.
Domain theory in the ALEA library:
https://www.lri.fr/~paulin/ALEA/
There is also this library:
http://research.microsoft.com/pubs/81147/domains.pdf

On Sun, May 11, 2014 at 1:03 AM, Aaron Stump <aaron-stump at uiowa.edu> wrote:
> Hello, Clarissa.
>
> Others on this list likely have much more complete developments, but I did
> write up the basic definitions for domain theory, and proved that ℕω is a
> domain (using a postulate for the limited principle of omniscience).  It
> would be quite a bit more work to get to a denotational semantics of While
> from what I have.  You can find my code (now) linked from the Software
> section of my web page (http://homepage.cs.uiowa.edu/~astump/).  Just in
> case this is better than nothing.  :-)
>
> Cheers,
> Aaron
>
> On 05/10/2014 01:41 PM, Clarissa Littler wrote:
>
> Hi there,
>
> So this isn't a pressing need or anything, but I've been wondering if anyone
> has done some kind of development of domain theory suitable for denotational
> semantics? Something maybe along the lines of an Agda version of
> dl.acm.org/citation.cfm?id=1616090 , where you use a coinductive lifting
> monad to represent non-termination. Cursory google searching didn't reveal
> anything.
>
> Cheers,
> Clarissa
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>