[Haskell-cafe] formal semantics

Aaron Tomb aarontomb at gmail.com
Sat Aug 25 18:12:26 CEST 2012


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:


And there's a talk about it here:


I think David is working from essentially the same goals you have in mind.


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

More information about the Haskell-Cafe mailing list