Stories by clarus

Extracting verified C++ from the Rocq theorem prover at Bloomberg

The new tactic engine of Coq 8.5

150,000 penguins die because of giant iceberg

Proving false in Coq using an implementation bug

POPL 2012 links of papers