Dmitry Rozplokhas and Dmitry Boulytchev: Certified Semantics for Disequality Constraints

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. We extend our proof of search completeness to this language extension. The description and proofs are certified in Coq and a correct-by-construction interpreter is extracted.

Forum Full Abstract

Leave a comment