C

cfml2

Separation Logic with Characteristic Formulae Entirely within Coq