clarus's submissions | Hacker News

1.		Extracting verified C++ from the Rocq theorem prover at Bloomberg (bloomberg.github.io)
		3 points by clarus 2 days ago \| past \| 1 comment
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