Certified Semantics for Relational Programming
Programming Languages
2020-09-18 v2
Abstract
We present a formal study of semantics for the relational programming language miniKanren. First, we formulate a denotational semantics which corresponds to the minimal Herbrand model for definite logic programs. Second, we present operational semantics which models interleaving, the distinctive feature of miniKanren implementation, and prove its soundness and completeness w.r.t. the denotational semantics. Our development is supported by a Coq specification, from which a reference interpreter can be extracted. We also derive from our main result a certified semantics (and a reference interpreter) for SLD resolution with cut and prove its soundness.
Keywords
Cite
@article{arxiv.2005.01018,
title = {Certified Semantics for Relational Programming},
author = {Dmitry Rozplokhas and Andrey Vyatkin and Dmitry Boulytchev},
journal= {arXiv preprint arXiv:2005.01018},
year = {2020}
}