Certified Semantics for Disequality
We present an extension of our prior work on certified semantics for core miniKanren, introducing disequality constraints in the language. Semantics is parameterized by an exact definition of constraint stores, allowing us to cover different implementations, and we provide a list of sufficient conditions on this definition for search completeness. We also give two examples of concrete implementations of constraint stores that satisfy those sufficient conditions. The description and proofs are partially certified in Coq and a correct-by-construction interpreter is extracted.