This repository contains proofs verifying that the partial abort semantics is equivalent to the full abort semantics for various STM implmementations.
- Use the ICFP15 branch for TL2 semantics
- Use JFP-Proofs branch for TinySTM semantics
lematt1991/ICFP15-Coq-Proofs
Proofs of correctness for "Partial Aborts for Software Transactional Memory" formalized in Coq
Coq