Jason (jcreed) wrote,

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.

  • (no subject)

    Apartment move finally completely done! Lugged air conditioner from old apartment to new, delivered bookshelf I didn't want to akiva, downstairs…

  • (no subject)

    Had a good bunch of discussions with Sean and Alyssa at work. Supposed to be stupid hot this weekend when we were planning to do the final cleanup of…

  • (no subject)

    Put kitchen table together, got K's desk set up in a useful place for her. Had dinner at a Thai place past the train a ways.

  • Post a new comment


    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded