Unification for Subformula Linking under Quantifiers
summary
Proposes Quantifying on the Uninstantiated, a unification-based algorithm that retroactively turns Evars found during matching into existential quantifiers, so it finds the simplification that provably follows from hypotheses under quantifiers rather than producing spurious equalities or failing to link. Implements the algorithm in Coq for Iris and diaph frame, demonstrates it solves the “last day of some year” counterexample that ACTA cannot handle and profin mishandles, proves it sits between ACTA and profin in power, and integrates with the iframe tactic to automate framing.
AI-written summary · about
chapters (15)
- 0:00Subformula linking intro
- 1:54How linking systems work
- 3:17Separation logic linking
- 5:49Quantifier challenges
- 7:36Core judgment simplifications
- 9:24Implication and disjunction rules
- 10:27Profin vs ACTA comparison
- 12:58Unification example walkthrough
- 14:46Limitations of quantifier rules
- 16:33New rule: quantification + instantiation
- 18:40Coq implementation details
- 20:53Retroactive quantification
- 21:14ACTA vs Profin comparison
- 21:38Improving iframe techniques
- 22:00Q&A
related talks
16mCounterexample Driven Quantifier Instantiations with Applications to Distribute...
14mSynthesizing Implication Lemmas for Interactive Theorem Proving
01h 05mVerifying Infinitely Many Programs at Once
19mProof Automation for Linearizability in Separation Logic
26mUnfolding Expressions for Gradual Verification
20mAutomating Unrealizability Logic: Hoare-style Proof Synthesis for Infinite Sets of(…)
14mQuantified Underapproximation via Labeled Bunches
20mUnifying compositional verification and certified compilation with a three-dimensional(…)