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.
You may also like
In this paper we research methods of supercompilation in the context of relational program specialization. We implement a supercompiler for miniKanren with […]
Evidential transactions (ETs) provide auditable and composable evidence that serves as a witness or a proof that a transaction has been correctly […]
Runtime verification (RV) consists in dynamically checking event traces generated by single runs of a system against a formal specification; such a […]
Forum Slides Attachments TEASE-LP_Sattler (7 MB)