By William E. Bird and Daniel P. Friedman, from WSFP 2007, available from William E. Bird’s website:
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.
Scheme source files can be found here.