A Fresh Name in Nominal Logic Programming
William E. Byrd, Daniel P. Friedman · 2007
We present ! Kanren, an embedding of nominal logic programming in Scheme. ! Kanren is inspired by ! Prolog and MLSOS, and allows programmers to easily write interpreters, type inferencers, and other programs that must reason about scope and binding. ! Kanren subsumes the functionality, syntax, and implementation of miniKanren, itself an embedding of logic programming in Scheme. We present the complete implementation of ! Kanren, written in portable R 5 RS Scheme. In addition to the implementation, we provide introductions to miniKanren and ! Kanren, and several example programs, including a type inferencer for the simply typed -calculus.