Submitted the LFMTP paper! That knocks off one of my three big things to get done by the end of this week, the other two being speaking skills and the HyLo paper. After that, it's a mixture of trying to head towards thesis proposal, and maybe a POPL submission if Frank and I can figure out how to extend the crazy labelled stuff in the LFMTP submission to dependent types. At the end of our meeting today he laughed and said he was finally beginning to be infected by my, and I quote, "gloom and doom" attitude about the prospects for that actually working. At least I'm glad I succeeded in expressing the technical content of my intuitions on the subject for once. Conversely, though, after I left the meeting I had idea that made me suddenly feel a little less doomed about how it might work after all. The idea is heavily inspired by the trick that seemed to make the hybrid dependent system more tractable (and come to think of it this goes all the way back to the trick that made the proof irrelevance stuff in my senior thesis work!) namely striving to make the type-kinding judgment as abasolutely mundane and conservative as possible, even while adding whizzy gadgets to the the object-typing judgment.