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

Autor:	Maggesi, Marco, Nocentini, Massimo
Rok vydání:	2020
Předmět:	Computer Science - Programming Languages
Druh dokumentu:	Working Paper
Popis:	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. Comment: Accepted for communication to miniKanren 2020 - miniKanren and Relational Programming Workshop
Databáze:	arXiv
Externí odkaz:	http://arxiv.org/abs/2007.04691 Zobrazit plný text záznamu View this record from Arxiv