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