Made some progress on the twelf proof, but I encountered a hole where I least expected it. Unlike some of my old bugs, this one at least is pointing somewhat clearly towards a solution.
I just found a paper from 2002 that I fear covers much of what I was hoping to push into my yet-hardly-conceived thesis proposal. Grr.
Class this morning was interesting; it is the final official class of the course, but Karl has
And speaking of non-required lectures during finals week, I am aiming for 4:00pm next thursday (a week from today) for giving the little intro talk about Twelf that I've been working on, location still to be determined. Intended audience includes that sort of people who have, say, heard of dependent types but are still confused and frightened by them. Pretty much anyone in HOT is already more advanced than this, likely as not, and that's just as well. In the worst case you might be bored for the first ten minutes.
