Formal semantics for Core?

Don Stewart dons at
Thu Dec 10 17:01:46 EST 2009

> On 11/30/09, Matthijs Kooijman <matthijs at> 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):

Note also, Simon Winwood's prototype executable semantics for Core in the
Twelf theorem prover:

-- Don 

More information about the Glasgow-haskell-users mailing list