Kanren Light: A Dynamically Semi-Certified Interactive Logic Programming System
share
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 mechanism for enabling the logic programming style for reasoning and computing in a theorem prover, and a framework for writing logic programs that produce solutions endowed with a formal proof of correctness.
READ FULL TEXT
