Jason (jcreed) wrote,
Jason
jcreed

I'm really getting low on sleep lately, but for no good reason. It's not like I'm stressed out and have to stay up really late working, I just keep staying up a bit later and waking up at the same time out of class-going necessity.

Had a somewhat informational meeting with Frank. All the little details of the Twelf codebase are still gradually making more sense. Much remains for me to understand on the metalogic side of things, but maybe I'll get around to studying it harder-core eventually.

Went to Joe Mama's after-11 half-price with combinator, pete, and dan blandford. Got the penne and sausage and actually mostly finished it this time.

Got a lot of hacking on Twelf done in the afternoon and after dinner. As of 3:00am, The "canonically weird" irrelevance unification problem

Ex Y . [x/a] c * x =? [x/a] Y

finally is solved correctly by my hacked copy
of Twelf, modulo the uninstantiated new evar
being left as a "dangling deBruijn index". I
should easily be able to fix that, though.
Subscribe
  • Post a new comment

    Error

    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

  • 1 comment