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
-
Notifications
You must be signed in to change notification settings - Fork 1
lematt1991/ICFP15-Coq-Proofs
Folders and files
| Name | Name | Last commit message | Last commit date | |
|---|---|---|---|---|
Repository files navigation
About
Proofs of correctness for "Partial Aborts for Software Transactional Memory" formalized in Coq
Topics
Resources
Stars
Watchers
Forks
Releases
No releases published
Packages 0
No packages published