Advisor meeting: gave an extremely bad summary of [Kosaraju 82]. But, hey, it reminded me which places I don't really understand so well. Sketched the proof that bangs need only occur top-left. Frank was somewhat mystified by the technique, which I admit is a kind of strange way of doing things, since it was pretty heavily inspired by a proof from complexity theory that the hierarchy collapses down to Sigma_2 if SAT in P/poly, using a formal notion of "good advice".
The good news is that there's a cleaner proof. The bad news is that it's someone else's. Doing a bunch of google searches after the meeting (since Type Systems was cancelled for some unknown reason) I found that Virgile Mobil's PhD thesis was about phase semantics and MELL, and its (English) abstract claimed that it made substantial steps towards showing that MELL was decidable. The thesis itself was in French, though. Bit of a bummer that. Not entirely discouraged, (it's not that hard to see that things like "Reseaux de Petri et Systemes d'addition de vecteurs" are "Petri Nets and Vector Addition Systems") however, I skimmed through it, and found on page 28 the statement of a theorem that looked very much like the one I had spent the last week proving.
After a bit of babelfish and bugging rjmccall, I figured out that it was in fact the same result (only stronger) using a very similar proof (only cleaner). Oh well. I'm happy that there is a clean way of doing it; instead of making a big ball of constraints that characterize the fixpoint of a certain process like I did, he just iterates the process repeatedly and has a trivial proof (just by the finiteness of a certain set) that it has to terminate, i.e. reach a fixpoint.
Apart from pure, undiluted geekery nearly saturating my every waking moment, cdinwood dragged me to Phipp's conservatory to see the Japanese-Chrysanthemum-Festival-themed exhibit. It was neat. Oh, and there was D&D. I made shocker-lizards go splat against the wall.