Add reference about Core's operational semantics.

diff --git a/Chapters/Normalization.tex b/Chapters/Normalization.tex
index f11788f4348fff5082a7a79bc5290057489b50d1..4f4ee15a12d6b8a4aac416d4f14bcac1fe0c090b 100644 (file)
--- a/Chapters/Normalization.tex
+++ b/Chapters/Normalization.tex
@@ -2354,9 +2354,9 @@
       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

diff --git a/Report.bib b/Report.bib
index a2e5417f69731a40fb65a71e36776385d8b19678..3e64e11410bc1dd802dc09255e1ba7467d615d0e 100644 (file)
--- a/Report.bib
+++ b/Report.bib
@@ -80,4 +80,15 @@
  address = {New York, NY, USA},
 }
 
-% vim: set paste:
+@inproceedings{sulzmann07,
+ author = {Sulzmann, Martin and Chakravarty, Manuel M. T. and Jones, Simon Peyton and Donnelly, Kevin},
+ title = {System F with type equality coercions},
+ booktitle = {TLDI '07: Proceedings of the 2007 ACM SIGPLAN international workshop on Types in languages design and implementation},
+ year = {2007},
+ isbn = {1-59593-393-X},
+ pages = {53--66},
+ location = {Nice, Nice, France},
+ doi = {http://doi.acm.org/10.1145/1190315.1190324},
+ publisher = {ACM},
+ address = {New York, NY, USA},
+}