Hi,
Last summer, as part of the Summer of Code, David Lazar formalized a
significant portion of Haskell 98 in the K framework. You can find the
code here:
https://github.com/davidlazar/haskell-semantics
And there's a talk about it here:
http://corp.galois.com/blog/2012/1/12/new-tech-talk-video-formalizing-haskell-98-in-the-k-semantic.html
I think David is working from essentially the same goals you have in mind.
Aaron
On Thu, Aug 23, 2012 at 9:23 AM, Ramana Kumar <ramana.ku...@cl.cam.ac.uk> wrote:
> Dear Haskell Cafe
>
> I'm looking for information on past and current attempts to write semantics
> for Haskell.
> Features I'm particularly interested in are:
>
> formal
> mechanised
> maintainable
> up to date
>
> Of course, if nothing like that exists then partial attempts towards it
> could still be useful.
>
> My ultimate aims include:
>
> Make it viable to define Haskell formally (i.e. so mechanised semantics can
> take over the normative role of the Haskell reports).
> Write a verified (or verify an existing) Haskell compiler (where verified
> means semantics preserving).
>
> Cheers,
> Ramana
>
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe@haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
