The paper on System FC [1] has an operational semantics. Would that do? Simon [1] http://research.microsoft.com/~simonpj/papers/ext-f | -----Original Message----- | From: glasgow-haskell-users-bounces@haskell.org [mailto:glasgow-haskell-users- | bounces@haskell.org] On Behalf Of Matthijs Kooijman | Sent: 30 November 2009 19:28 | To: GHC-users | Subject: Formal semantics for Core? | | Hi All, | | I was wondering if there are any formal semantics defined for GHC's core | language? I'm working with some core to core rewriting passes for which I'd | like to verify the soundness, but that would require some formal definition of | the Core semantics of sorts... | | Gr. | | Matthijs

On 11/30/09, Matthijs Kooijman wrote:

Hi All,

I was wondering if there are any formal semantics defined for GHC's core language? I'm working with some core to core rewriting passes for which I'd like to verify the soundness, but that would require some formal definition of the Core semantics of sorts...

It may not be exactly what you're looking for, but the extcore package includes a typechecker and interpreter that provide an executable static and dynamic semantics for External Core (which is similar to the Core language that GHC uses externally, but not quite the same): http://hackage.haskell.org/package/extcore Cheers, Tim -- Tim Chevalier * http://cs.pdx.edu/~tjc * Often in error, never in doubt "Do we learn from our mistakes? I surely hope not / Takes all the fun out of making them again." -- Trout Fishing In America