This page is about a new soundness proof for concurrent separation logic (CSL) in terms of the standard operational semantics. The new proof gives a direct meaning to CSL judgments, explains clearly the problem with the conjunction rule and "precise" resource invariants, and can easily be adapted to handle extensions of CSL, such as permissions and storable locks, as well as more advanced program logics, such as RGSep.
Viktor Vafeiadis: Concurrent separation logic and operational semantics.
In MFPS 2011.
Click here for the tarball [.zip], prepared with Isabelle version 2009-2, or browse the pretty-printed sources online: