Types, Atomic Actions and Dirac's Notation

My recent work has dealt quite alot with Hoare types and how they can be used to reason about concepts like linearizability. This has been a bit rough, for several reasons. Hoare types are fine for reasoning about sequential consistency in programs. For instance, in the following simple (and infomal, and probably incorrect by "true" Hoare logic) example:

x ← [l] : { v : Int = [l] } Unit { x : Int = v }
[l] ← x + 1 : { x : Int } Unit { [l] = x + 1 }
x : { x : Int } x { }

the types can be combined by the rules of Hoare logic into the type { v : int = [l] } v { [l] = v + 1 }.

But in concurrency, this isn't what we want. We don't really care about one step guaranteeing the preconditions of another. We care about observing properties and causing effects. It's a subtle, but distinct difference, and it seems related to what I was talking about earlier with differentiation of propositions. Observing a property is when some proposition in the outside world causes a change in the eventual result of the term. Causing an effect is when some proposition is changed. So basically, you have the properties you observe, the effects you cause, and a change of types (as in, a before type, and an after type)

Of all ways to represent this, Dirac's notation comes to mind. The representation of effects would go something like this: 〈 properties observed | effects caused 〉. So, for instance, we might type an atomic counter as 〈 v : Int = [l] | [l] = v + 1 〉. Now, we also need to add the type of the term before the action, versus the type after. So, the type might look something like this: Int〈 v : Int = [l] | [l] = v + 1 〉v. This is, of course, a simplification. In a real dependent type system, expect something like this:

Π l : Int Ref.Π x : Int. Int〈 [l] = v | [l] = v+1 〉{ y : Int. y = v }

The other benefit of this is that it allows sequences of atomic actions to be differentiated from individual ones. The counter I gave above would be typed as something like (in the simpler form):

Int〈 v : Int = [l] | 〉v ; v〈 | [l] = v + 1 〉v

The best part of all this is that I have a pretty good idea how to get these automatically from the sequences of Hoare-typed terms and dependently-typed heaps I've been working with in all my writings on this subject, and that method is a propositional differentiation function...

I told you, it all comes together in the end.