| 1. | | Extracting verified C++ from the Rocq theorem prover at Bloomberg (bloomberg.github.io) |
| 129 points by clarus 64 days ago | past | 39 comments |
|
| 2. | | The new tactic engine of Coq 8.5 (inria.fr) |
| 3 points by clarus on Feb 14, 2016 | past |
|
| 3. | | 150,000 penguins die because of giant iceberg (theguardian.com) |
| 1 point by clarus on Feb 13, 2016 | past |
|
| 4. | | Proving false in Coq using an implementation bug (github.com/clarus) |
| 125 points by clarus on March 24, 2015 | past | 61 comments |
|
| 5. | | POPL 2012 links of papers (claret.me) |
| 1 point by clarus on Dec 11, 2011 | past |
|
