December 9th, 2008

beartato phd

(no subject)

Made a ton of good progress on HLF implementation today, got my first (just barely) nontrivial Server OK doing coverage checking on a substructural program. Unification still has some bugs but I was able to work around them. A major thing I found out that I didn't expect is that it's quite important to mark (or at least otherwise infer) which type families are going to be treated as linear or not --- for otherwise you get all these spurious dependencies on modal worlds in the subordination relation that require b.s. strengthening lemmas.

So as a bit of a reward went and saw "The Boy With the Striped Pajamas", (8/10). Very effective way of showing the horrors of war through the eyes of a small child. Depressing as all hell, though. I mean... damn. I need to switch things up to some happier movies.