  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.
