KCC is certainly an achievement, but it doesn't subsume Robert's work. If you look into the linked thesis you'll find that a lot of the work deals with finding

KCC is certainly an achievement, but it doesn't subsume Robert's work. If you look into the linked thesis you'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). 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. 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).