On 2/12/07, Robert Dockins
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
I was also neglectful in not mentioning this paper: http://www.cse.unsw.edu.au/~chak/papers/SCPD07.html System F with Type Equality Coercions Martin Sulzmann, Manuel M. T. Chakravarty, Simon Peyton Jones, and Kevin Donnelly. In G. Necula, editor, Proceedings of The Third ACM SIGPLAN Workshop on Types in Language Design and Implementation, ACM Press, 2007. which describes System FC, which is the current incarnation of Core in GHC, and in fact that paper *does* give an operational semantics for it. Cheers, Kirsten -- Kirsten Chevalier* chevalier@alum.wellesley.edu *Often in error, never in doubt "It's important for us to explain to our nation that life is important. It's not only life of babies, but it's life of children living in, you know, the dark dungeons of the Internet." -- George W. Bush