To be able to formally show that each transformation properly
preserves the meaning of every expression, we require an exact
definition of the \emph{meaning} of every expression, so we can
- compare them. Currently there seems to be no formal definition of
- the meaning or semantics of \GHC's core language, only informal
- descriptions are available.
+ compare them. A definition of the operational semantics of \GHC's Core
+ language is available \cite[sulzmann07], but this does not seem
+ sufficient for our goals (but it is a good start).
It should be possible to have a single formal definition of
meaning for Core for both normal Core compilation by \GHC and for