<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 &#8469;&#969; is a domain (using a postulate for the limited principle of
    omniscience).&nbsp; It would be quite a bit more work to get to a
    denotational semantics of While from what I have.&nbsp; 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>).&nbsp; Just in case this is
    better than nothing.&nbsp; :-)&nbsp; <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>