Stream: Coq users

Topic: Shallow embedding and custom entailment procedure


view this post on Zulip towokit928 (Sep 11 2023 at 08:51):

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