[This session is part of the miniKanren Confo colocated with Clojure/West.]
Nominal logic simplifies reasoning about scope and binding, so that implementing interpreters and type inferencers is almost as easy as on paper. Inspired by alphaKanren, we embed nominal logic programming into Clojure. Unlike alphaKanren, which is incompatible with cKanren, core.logic.nominal extends core.logic. In this talk, I will introduce the core.logic.nominal primitives (fresh, tie, hash), show some examples (quine generator, typed lambda calculus, theorem prover) and highlight our implementation.
Sign in to add slides, notes or videos to this session