Kanren Light: A Dynamically Semi-Certified Interactive Logic Programming System

Marco Maggesi, Massimo Nocentini

We present an experimental system strongly inspired by miniKanren, implemented on top of the tactics mechanism of the HOL~Light theorem prover. Our tool is at the same time a mecha…