12 ms·

Here is a Coq formalization of C11: http://robbertkrebbers.nl/research/ch2o/ http://robbertkrebbers.nl/research/ch2o/ It only covers a large fragment of C11, bu

Here is a Coq formalization of C11: http://robbertkrebbers.nl/research/ch2o/ http://robbertkrebbers.nl/research/ch2o/ It only covers a large fragment of C11, but they formalized the operational, axiomatic, and executable semantics and proved that these correspond to each other.

tom_mellior 9y ago
Yes, and there are other formalizations as well. But none of them (as far as I am aware) formalize the undefined parts in the way the featured article does. I think comparing projects with different goals and then saying "the differences must be due to the tools used" isn't solid reasoning.