Abstract

The promise of logic programming is that programs can be written relationally, without distinguishing between input and output arguments. Relational programs are remarkably flexible—-for example, a relational type-inferencer also performs type checking and type inhabitation, while a relational theorem prover generates theorems as well as proofs and can even be used as a simple proof assistant. Unfortunately, writing relational programs is difficult, and requires many interesting and unusual tools and techniques.

In this talk I will discuss miniKanren, a language specifically designed for relational programming. miniKanren is designed to be easily hackable, and has been ported from Scheme to many languages, including Racket, Clojure, Python, Haskell, Scala, Ruby, and JavaScript. miniKanren features complete search, relational arithmetic, nominal unification (inspired by the work of Andrew Pitts and his students at Cambridge), and various constraint extensions. I will demonstrate an environment-passing Scheme interpreter and a term reducer for combinatory logic, both written in miniKanren, and show how both can be used to perform program synthesis.

Bio:

William E. Byrd is a Research Associate in the U Combinator programming languages research group at the University of Utah. He received his PhD from Indiana University in 2009, under Daniel P. Friedman. He is co-author of The Reasoned Schemer, and co-designer of several declarative languages: miniKanren (logic programming), Harlan (GPU programming), and Kanor (cluster programming).