论文标题
关系编程的认证语义
Certified Semantics for Relational Programming
论文作者
论文摘要
我们为关系编程语言Minikanren提供了一项关于语义的正式研究。首先，我们制定了一种典型的语义，该语义与确定逻辑程序的最小Herbrand模型相对应。其次，我们提出了模拟交错的操作语义，是Minikanren实施的独特特征，并证明了其健全性和完整性W.R.T.表示语义。我们的开发得到了COQ规范的支持，可以从中提取参考解释器。我们还从我们的主要结果中得出了SLD分辨率的认证语义（和参考解释器），并证明了其健全性。
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.
