Had class before that, in which Karl covered CPS translation. I still asked a bunch of really dumb questions during class, since I am unfortunately still in the 90%-knowing-what-CPS-conversion-is but 10%-still-fucking-up-the-intuition-for-i
Read most of Aleskey's recent JFP paper with Karl and Frank about using Monads to enforce information-flow security and whatnot, as per helping him satisfy the writing requirement by me reviewing it and filling out the little form. I've never been very excited about all these notions of low and high security levels and non-interference proofs --- it all feels very military-minded with classification levels and all --- but it's a neat paper.
I bashed through another 50 frames of this Flash thing. At this point I am starting to realize that I should maybe make absolute certain that I have an audience other than Erika and her posse so's I can at least figure out if the intended spoken part of the talk works. Akiva? Mkehrt? You guys or any of your interested theory wanker acquaintances still going to be around during finals week and not type-theoried out by Karl's extra GC lectures?
If any of y'all want to check out the new slides, (although maybe it would be considered SPOILERS for anyone intending to see me do the talk) they're here at the usual location. I've almost got up to the point where Twelf starts really doing its awesome meta-theoretical thing.
The live Twelf connection in the presentation finally had a concrete payoff. I was routinely running through viewing the last few slides I had written and Twelf choked at me, because I had made a typo in the example code. Score one more for mechanical verification! :)