Ian Wehrman has sent the following abstract for 11/11/09:
In this talk, I present a trace semantics based on graphs: nodes
represent the events of a program's execution, and edges represent
dependencies among the events. The style is reminiscent of partially
ordered models, though we do not generally require properties like
transitivity or acyclicity. Concurrency and sequentiality are defined
using variations on separating conjunctions, which are instances of
model theories of separation logic and bunched logic. The model has
pleasant algebraic properties, which follow from surprisingly simple
proofs. I present a number of theorems about the general model,
including the soundness of the laws of Hoare logic and the Jones
rely/guarantee calculus. No particular languages or applications are
studied; this is left to future work.