Met with Gopalan Nadathur today as part of the usual meet-with-the-visiting-speaker thing. Talked about the redundancy elimination stuff a little bit, but before that wasted some time talking about fiddly constructivity issues involved with SN that he seemed to be all to eager to brush aside. I still feel the precise choice of even the statement of the strong normalization property hides a subtle but important philosophical statement. People like Tom might argue that arguing about the definition of it is doubly pointless, since even proofs of it are already of ho-hum value levels. :)

Slowly squeezing bugs out of this toy compiler. It's interesting now that the bugs have moved beyond my total generalized naivete as to how to write a compiler, and are becoming involved more with the "actual" "semantics" of the "language" I'm compiling to. Being the total POS that javascript is, it has a crazy notion of scope that makes correct compilation of let-expressions very vexing. I may have to do some sort of CPS thing after all, or at the very least some renaming if I am to support variable shadowing at all. Also a couple of bugs in not correctly dealing with tuples the same way everywhere. I am still in a state right now where the compiled version of the parser is not working correctly, but it's time to go to sleep.