2011-05-25

simrob: selfie with a digital camera using reflection in a train window (Default)
2011-05-25 11:56 am
Entry tags:

Focus

Used a not-terrifically-worded question on MathOverflow and the fact that I had two hours to kill as an excuse to finally write out the cut-and-identity-based proof of the completeness of (weak) focusing for the negative fragment, where you don't have to admit that it's only weak focusing. I wrote out all the details in the Weak Focusing for Ordered Linear Logic tech report, but that TR has way the hell too much other stuff going on.