[Agda] Domain Theory Libraries for Agda?

[Aaron Stump]

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 N? 
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 
> <http://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

-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20140510/f9267253/attachment.html