<html>
<head>
<meta content="text/html; charset=ISO-8859-1"
http-equiv="Content-Type">
</head>
<body bgcolor="#FFFFFF" text="#000000">
Hello, Clarissa.<br>
<br>
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
(<a class="moz-txt-link-freetext" href="http://homepage.cs.uiowa.edu/~astump/">http://homepage.cs.uiowa.edu/~astump/</a>). Just in case this is
better than nothing. :-) <br>
<br>
Cheers,<br>
Aaron<br>
<br>
<div class="moz-cite-prefix">On 05/10/2014 01:41 PM, Clarissa
Littler wrote:<br>
</div>
<blockquote
cite="mid:CAH-5Xsc_+4Xv4evrvKnYLc9MmQt8fJNymzSg27ub2LqhRv7AaA@mail.gmail.com"
type="cite">
<div dir="ltr">Hi there,
<div><br>
</div>
<div>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 <a
moz-do-not-send="true"
href="http://dl.acm.org/citation.cfm?id=1616090">dl.acm.org/citation.cfm?id=1616090</a>
, where you use a coinductive lifting monad to represent
non-termination. Cursory google searching didn't reveal
anything.</div>
<div><br>
</div>
<div>Cheers,</div>
<div>Clarissa</div>
</div>
<br>
<fieldset class="mimeAttachmentHeader"></fieldset>
<br>
<pre wrap="">_______________________________________________
Agda mailing list
<a class="moz-txt-link-abbreviated" href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a>
<a class="moz-txt-link-freetext" href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a>
</pre>
</blockquote>
<br>
</body>
</html>