October 3rd, 2003

beartato phd

(no subject)

Hmm. So I actually can code up the typing rules for proof irrelevance inside good ol' vanilla LF, but it requires an ugly predicate of kind ((var -> tm) -> var -> tm) -> ((var -> tm) -> var -> tm) -> type whose definition has size proportional to the size of the language, and the whole affair is hideously anti-modular. A small victory nonetheless. I should get back to real work, though.
beartato phd

(no subject)

lincoln3 mentions occasionally how he copes with colds and flus going around by simply not ever getting sick. Sounds like a good plan. Not sure if it's working out for me. I feel vaguely feverish and headachey. I've been eating poorly, though. McDonald's and salty vending-machine food so far today. Got some japanese homework done, looked at fellowship application stuff (application essays yech yech yech) worked on research some. I should get back in the habit of spending more time in the library. It is actually somewhat conducive to me getting work done, as long as there aren't people around loudly sniffing and snorting and horking up mucus. Which now and then there are.

Office hour score still stands at 0-for-god-knows-how-many. Need to do some grading this weekend.

Tonight: music with the kids.
beartato phd

(no subject)

Music went really well. I don't think I will ever completely tire of the good ol' Am-G-F-E7 progression. It was the one I used when I first started learning to improvise, and it still sounded great to hear victoria and dave play over it tonight.

But now I am exhausted. Plans include sleep, and then housecleaning in the morning.