KCC is certainly an achievement, but it doesn&#x27;t subsume Robert&#x27;s work. If you look into the linked thesis you&#x27;ll find that a lot of the work deals with finding high-level descriptions of the C semantics. A major part of CH2O is developing an axiomatic semantics for large parts of the C language, which is novel (as far as I know).<p>There are a few real gems in this thesis. In particular, I really liked the explanation of sequence points in terms of separating conjunction. This is much more compact than the imperative program to decide definedness that is implicitly described in the C standard.<p>The proofs of equivalence between the different semantic descriptions also go beyond what KCC does, or for that matter what you can do within the K framework (at the moment).