max_ambiguity was on the same bus as me and I didn't recognize her, and she was really offended. Sorry!I twelfed up a proof of cut elimination for my peculiar version of a focussed sequent calculus, where instead of saying
i) first you have to decompose all the asynchronous stuff
ii) then you have to decompose some run of synchronous stuff "all the way"
you say
i) you must decompose something (be it asynchronous or synchronous) "all the way", until you reach a shift operator (which may just be permission pause, "shifting" from positive to positive or negative to negative)
ii) having made this restriction, notice after the fact that you might as well decompose asynchronous monopoles things first, since they're invertible.
Not making the system so finicky as to demand eager decomposition of anything makes its cut elimination proof really simple ~ it's only like a couple hundred lines of twelf with comments, and it's basically O(1) overhead in length compared to the standard cut elim proof.
Also finished reading Arjouni's short story collection "Idiots". It was okay — I didn't have any explicit expectations after picking it up at random from the library because I liked the cover, but it was a bit disappointingly mundane following Barthelme, and it's hard not to be annoyed at writers writing about writing (which Arjouni does constantly) unless they do it really well.