Kanren Light: A Dynamically Semi-Certified Interactive Logic Programming System
Marco Maggesi, Massimo Nocentini
TL;DR
Kanren Light is an experimental logic programming system integrated with HOL Light, enabling reasoning and computation with formally certified solutions within a theorem prover environment.
Contribution
It introduces a semi-certified, interactive logic programming framework built on HOL Light, combining logic programming with formal proof guarantees.
Findings
Provides a new mechanism for logic programming within HOL Light
Enables producing solutions with formal correctness proofs
Integrates logic programming seamlessly into theorem proving environment
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Logic, Reasoning, and Knowledge · Formal Methods in Verification