alphaKanren: A fresh name in nominal logic programming

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.

1 Response to “alphaKanren: A fresh name in nominal logic programming”


  1. 1 Crystle September 18, 2015 at 4:01 pm

    You really make it appear really easy with your presentation but I find this topic to
    be actually one thing which I think I’d by no means understand.
    It seems too complex and extremely wide for me. I’m taking a look forward in your subsequent put
    up, I will attempt to get the hold of it!


Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s





%d bloggers like this: