clarus
- Karma
- 0
- Created
- ()
- Submissions
- 0
- Extracting verified C++ from the Rocq theorem prover at Bloomberg (bloomberg.github.io)
- The new tactic engine of Coq 8.5 (coqhott.gforge.inria.fr)
- 150,000 penguins die because of giant iceberg (theguardian.com)
- Proving false in Coq using an implementation bug (github.com)
- POPL 2012 links of papers (guillaume.claret.me)