From 2c28bdc6ca8e883697d9640166bf17fb8a329cec Mon Sep 17 00:00:00 2001 From: Matthijs Kooijman Date: Sun, 6 Dec 2009 21:17:28 +0100 Subject: [PATCH] Add reference about Core's operational semantics. --- Chapters/Normalization.tex | 6 +++--- Report.bib | 13 ++++++++++++- 2 files changed, 15 insertions(+), 4 deletions(-) diff --git a/Chapters/Normalization.tex b/Chapters/Normalization.tex index f11788f..4f4ee15 100644 --- 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 a2e5417..3e64e11 100644 --- 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}, +} -- 2.30.2