Portable modulo signed arithmetic operations Pascal Cuoq on 26 February 2013
In a recent post, John Regehr reports on undefined behaviors in Coq! In Coq! Coq! Exclamation point! Coq is a proof assistant. It looks over your shoulder and tells you what remains to be done while you are elaborating a mathematical proof. Coq has been used to check that the...
Read More