I've been going through Xavier Leroy's program logic lectures. Here is the entailment definition for a shallowly-embedded separation logic. It's very elegant, but I'm not sure how to extend it with frame inference (see this, section 4.5), i.e. collecting the "leftover" assertions from a failed proof for use in subsequent proofs. Does this mean I have to use a deep embedding instead? Seeing as with a shallow embedding, I can't analyze the formulae on both sides of the entailment.

Last updated: Jun 22 2024 at 16:02 UTC