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.