Certified Semantics for Disequality
summary
Semantics extends core miniKanren with disequality by parameterizing the operational rules over an abstract constraint store and proving completeness under five sufficient conditions on that store definition. The development is mechanized in Coq-certified proofs and yields an extracted correct-by-construction interpreter. Two concrete stores are given: a trivial pair-list store that can produce contradictory answers, and a practical substitution-based store that works provided bound variables never reappear, with formal conditions and proofs spelled out.
AI-written summary · about
chapters (11)
- 0:00Intro
- 1:43Disequality constraints
- 3:45Base Language
- 5:35Operational semantics: objective
- 7:32Operational semantics: form
- 8:48Operational semantics: rules for basic goals
- 9:27Operational semantics: other rules
- 10:23Semantics equivalence
- 11:58Sufficient conditions for completeness
- 14:09Example of implementation - a realistic one
- 15:47Applications
related talks
17mCalculational design of Incorrectness Separation Logic
30mSemantics-Guided Synthesis
56mOmnisemantics: Smooth Handling of Nondeterminism (Invited talk)
22mCategorical Semantics of Probabilistic Symbolic Execution
22mMechanised Semantics for Gated Static Single Assignment
19mCausality and Semantic Separation
20mCertified Abstract Machines for Skeletal Semantics
21mChecking Equivalence in a Non-strict Language