Certified Semantics for miniKanren
We present our project on development of certified operational semantics for miniKanren – embedded language for logic programming. In contrast to previous formal semantics for miniKanren, our variant models the interleaving search strategy – a distinctive feature of miniKanren implementation. New semantics may serve as a unified way of formal description of the search in core miniKanren and its various extensions. We use it to prove important non-trivial properties of the search, in particular, completeness w.r.t. the denotational semantics. To increase confidence in our (rather intricate) proofs we support the development with a Coq specification, from which certified reference interpreters can be extracted.