optimizations in the proof of adequacy of algorithmic
equality for the irrelevance system. I should whip up
a sample object language and prove a little represenation
adequacy theorem for it to get a feel for how quasi-canonical
objects should behave.
Mailed off UPenn application.
Zml in town. Lots of gaming going on in the lounge.
More old-skool people should be showing up sortly.
Shiue, mhock, christina-the-freshman, and I went to Krispy
Kreme in the former's car. Mmmoughnum... sweet, sweet
sugar-glazed lovin'.
