[Hoffmann+ 2013]の論理体系をCoqで形式化
Coqのバージョンは8.6.1である
- Basics.v : softwarefoundationsからのコピー
- Maps.v : softwarefoundationsからのコピー
- lang.v : プログラミング言語の定義
- stack.v : プッシュの証明
- LICENSESF : Basics.vとMaps.vにはこのライセンスが適用される(softwarefoundationsからのコピー)
Coqのチュートリアル http://www.cis.upenn.edu/~bcpierce/sf
[Hoffmann+ 2013]の論文 http://www.cs.cmu.edu/~janh/papers/lockfree2013.pdf