On Sat, Aug 25, 2012 at 3:38 PM, Jay Sulzberger
This is good. I will look at the references given in this thread. The account at
http://web.archive.org/web/20060206074101/http://www.cse.ogi.edu/~mpj/thih/T...
is, I think, one part of what I was looking for.
The book I recommend (although now I feel like a bad person because I haven't read all of it :-(.., is "The Implementation of Functional Languages," http://research.microsoft.com/en-us/um/people/simonpj/papers/slpj-book-1987/... I remember finding it quite approachable, although for the immediate need of trying to implement *Haskell* in a verified environment, it might not be immediately helpful, it's really good background reading on the subject that will be imperative should you want to do such things (and written around the time when Haskell was congealing, so should be representative-ish of the attitudes underlying Haskell's design at the time: graph reduction, compiling pattern matching, translating high level lamda languages to core semantics). kris