My categorical intuition tells me that most of what is going on there is really a category C whose objects are pieces of data, whose arrows are patches, equipped with a functor to a group G which is the "names" of those patches. That is, when I have a square
v A / \ B / \ v v \ / B \ / A v
Clearly the two copies of A (resp. two copies of B) are not the *same* change, but they have the same intention. The idea would be that the functor maps these down to the same group element.
neelk was talking to me for a bit about his attacking of separation logic with a labelled sequent calculus. Funny how (I → I) * A does entail (I → I) ^ A in that system, but (apparently) not in bunched logic. His axiomatization of the nontrival equality theory that involves hypothetical equalities doesn't permit the unificationesque decompositions that would allow you to infer a * b = a * c |- b * c, but I can't come up with a raw proposition that would lead to such an equational test.