
On Feb 12, 2007, at 1:31 PM, Kirsten Chevalier wrote:
On 2/11/07, Matt Roberts
wrote: - Exactly what are the operational and denotational semantics of core?
Since I don't think this question has been answered yet, here's a mailing list post from Simon PJ that probably answers it: http://www.haskell.org/pipermail/glasgow-haskell-users/2003- February/004849.html
That's from 2003, but I don't think the answer has changed since then. If you wrote down a precise operational and/or denotational semantics for Core, you'd probably have a research paper. (Especially if you proved that GHC actually obeys that semantics...) (Disclaimer: my name isn't Simon.)
At the risk of sounding self-promoting, I'd like to point out that the research paper I recently announced defines an intermediate language that is similar to GHC's core in some respects (they are both based on System F_omega). I give a full (call-by-name) operational semantics and type system for the language in my report [1]. You won't find any proofs in the paper, but they're on my medium-term agenda. There is also source code for an interpreter/ bytecode-compiler/shell for this intermediate language [2]. [1] http://www.cs.tufts.edu/tr/techreps/TR-2007-2 [2] http://www.eecs.tufts.edu/~rdocki01/masters.html
Cheers, Kirsten
Rob Dockins Speak softly and drive a Sherman tank. Laugh hard; it's a long way to the bank. -- TMBG