Correctness proof of a log-based semantics for software transactional memory with respect to a stop-the-world semantics, using Agda.
The exact version described in chapter 9 of my thesis is tagged as such. Futher refinements are on the master branch, including compatibility fixes for more recent versions of Agda and/or Nisse's standard library.
This current version typechecks with the development versions of the aforementioned as of 2013-05-11, but fails with Agda 2.3.2 (released on 2012-11-12) due to a couple of regressions.