Jason (jcreed) wrote,
Jason
jcreed

Meeting with Frank. Looks like my A^w := A^0 \oplus A^1 idea is pretty much shot to hell, since I can't even type the identity on A^w in the empty context. Oops. However, I received a more detailed explanation of one example of why dependency on linear variables seems like a valuable thing, namely the LLF encoding of cut elimination for the linear intuitionistic sequent calculus. Mmm, so many buzzwords in one sentence. So I think I will gain more enlightenment by meditating on that example in particular.

Went to type theory. Karl discussed N-ary products sum types void type yadda yadda yadda. Don't they teach this in undergrad? Sheesh. Everyone should be a PL weenie!

Worked on complexity theory homework. More difficult than I thought when I looked at it earlier, but then again more interesting than I thought, too. These are still the most rewarding homeworks I've had for a class in some time. It is actually genuinely satisfying pretty frequently to figure out the solutions.

D&D. Some stuff happened. Killed an earth elemental. Wandered around and talked to people. I feel very guilty about my attention span. Much doodling and thinking about complexity theory.

Went to Joe Mama's. Tasty, cheap food, good friends, bad puns. But few other things I ask from life.
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 

  • 6 comments