Jason (jcreed) wrote,

Was abruptly awakened at 6am. My cell phone is only not in vibrate mode when it's plugged into the wall, but it was at the time, charging, and actually played the custom tone I hacked into it a few days ago. Then: french toast. Mmm. Norm was also up early, for a chemistry test, apparently, so he got a couple slices also.

Went to part of theory lunch, where they discussed the "primes is in P" paper. I got lost about half-way through the correctness proof (but at least the algorithm itself and the proof of polytime termination are pretty easy) and so I skipped out early. Turned in Type Systems homework. Went over part of a paper on the semantics of bunched logic during the class. Some times I realize how little category theory I really know. Must learn more about fibrations, indexed categories, ends and co-ends, Kan extentions. I think I'm finally beginning to feel at home with (symmetric) monoidal closed categories though. Exposure to substructural logics has helped a lot with that.

Anyway. Procrastinated a bit after type systems. Went to the ConCert meeting where Susmit was talking about oracle-based proof compression. Eleurgh. I see why Frank was trying to look for something a bit less dependent on the exact proof-search mechanism. Left that to work on machine learning homework. Machine learning homework SO BORING ARGH. At least I got to play with gnuplot a bit more. Plots using "with errorbars" look cute. Got the coding part done about 20, got the rest done at 22ish.

  • (no subject)

    Some further progress cleaning up the https://xkcd.com/1360/ -esque augean stables that is my hard drive. Tomato chicken I made a couple days ago…

  • (no subject)

    Did some personal archaeology. Helped a little with laundry. Threw some chicken, onions, tomato, stock, peppers in the slow cooker and hopefully…

  • (no subject)

    Dinner with akiva and dannel at nuevo portal in carroll gardens. Ate a pile of chicken stew and rice and beans and maduros, good times. I do miss…

  • Post a new comment


    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded