Jason (jcreed) wrote,

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.
Tags: movies, work

  • Post a new comment


    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

  • 1 comment