Re: Formal semantics for Core?

catamorphism:

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

Note also, Simon Winwood's prototype executable semantics for Core in the Twelf theorem prover: http://www.cse.unsw.edu.au/~sjw/non-cvs/code/coreLF.tar.gz -- Don