Partial Abort STM Proofs 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