[Haskell-cafe] formal semantics

[Ramana Kumar]

Thanks much Kristopher, Gershom, and Aaron, for the excellent pointers.
(Keep them coming, anyone else - maybe we can update the wiki..)
I will look into them in more detail soon.

On Sat, Aug 25, 2012 at 5:12 PM, Aaron Tomb <aarontomb at gmail.com> wrote:

> 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.Kumar at 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 at haskell.org
> > http://www.haskell.org/mailman/listinfo/haskell-cafe
> >
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20120825/40bd3658/attachment.htm>