Kanren Light: A Dynamically Semi-Certified Interactive Logic Programming System
Programming Languages
2020-07-10 v1
Abstract
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.
Keywords
Cite
@article{arxiv.2007.04691,
title = {Kanren Light: A Dynamically Semi-Certified Interactive Logic Programming System},
author = {Marco Maggesi and Massimo Nocentini},
journal= {arXiv preprint arXiv:2007.04691},
year = {2020}
}
Comments
Accepted for communication to miniKanren 2020 - miniKanren and Relational Programming Workshop