Re: [Haskell-cafe] formal semantics

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 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-haskel...

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 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