Thanks much Kristopher, Gershom, and Aaron, for the excellent pointers. (Keep them coming, anyone else - maybe we can update the wiki..)<br>I will look into them in more detail soon.<br><br><div class="gmail_quote">On Sat, Aug 25, 2012 at 5:12 PM, Aaron Tomb <span dir="ltr"><<a href="mailto:aarontomb@gmail.com" target="_blank">aarontomb@gmail.com</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi,<br>
<br>
Last summer, as part of the Summer of Code, David Lazar formalized a<br>
significant portion of Haskell 98 in the K framework. You can find the<br>
code here:<br>
<br>
<a href="https://github.com/davidlazar/haskell-semantics" target="_blank">https://github.com/davidlazar/haskell-semantics</a><br>
<br>
And there's a talk about it here:<br>
<br>
<a href="http://corp.galois.com/blog/2012/1/12/new-tech-talk-video-formalizing-haskell-98-in-the-k-semantic.html" target="_blank">http://corp.galois.com/blog/2012/1/12/new-tech-talk-video-formalizing-haskell-98-in-the-k-semantic.html</a><br>
<br>
I think David is working from essentially the same goals you have in mind.<br>
<span class="HOEnZb"><font color="#888888"><br>
Aaron<br>
</font></span><div class="HOEnZb"><div class="h5"><br>
On Thu, Aug 23, 2012 at 9:23 AM, Ramana Kumar <<a href="mailto:Ramana.Kumar@cl.cam.ac.uk">Ramana.Kumar@cl.cam.ac.uk</a>> wrote:<br>
> Dear Haskell Cafe<br>
><br>
> I'm looking for information on past and current attempts to write semantics<br>
> for Haskell.<br>
> Features I'm particularly interested in are:<br>
><br>
> formal<br>
> mechanised<br>
> maintainable<br>
> up to date<br>
><br>
> Of course, if nothing like that exists then partial attempts towards it<br>
> could still be useful.<br>
><br>
> My ultimate aims include:<br>
><br>
> Make it viable to define Haskell formally (i.e. so mechanised semantics can<br>
> take over the normative role of the Haskell reports).<br>
> Write a verified (or verify an existing) Haskell compiler (where verified<br>
> means semantics preserving).<br>
><br>
> Cheers,<br>
> Ramana<br>
><br>
><br>
</div></div><div class="HOEnZb"><div class="h5">> _______________________________________________<br>
> Haskell-Cafe mailing list<br>
> <a href="mailto:Haskell-Cafe@haskell.org">Haskell-Cafe@haskell.org</a><br>
> <a href="http://www.haskell.org/mailman/listinfo/haskell-cafe" target="_blank">http://www.haskell.org/mailman/listinfo/haskell-cafe</a><br>
><br>
</div></div></blockquote></div><br>