This summer school provides an introduction to relational programming, a pure form of logic programming in which programs are written as mathematical relations, erasing the distinction between "input" arguments and "output" values. Relational programming is a Turing-complete generalization of relational database languages like SQL and Datalog.
We will be programming in miniKanren (www.minikanren.org), an embedded domain specific language for constraint logic programming that is designed specifically for relational programming. miniKanren is the language used in the "The Reasoned Schemer" (MIT Press, 2005), and is the inspiration for Clojure's popular "core.logic" library. miniKanren is one of the languages described in "Seven More Languages in Seven Weeks: Languages That Are Shaping the Future" (Pragmatic Programmers, 2014).
In the course we will learn to write relational programs in miniKanren, explore the remarkable flexibility of these relations, and learn how miniKanren works. Students will implement miniKanren in a host language of their choice. We will write type inferencers and interpreters as miniKanren relations, see the Curry-Howard correspondence in action, and learn how a relational interpreter is a theorem prover over a specialized domain: the operational semantics of the language under interpretation. We will look at the latest research in miniKanren, and explore how a relational interpreter might be used for program synthesis, symbolic execution, and automatic test generation.
Students do not need prior experience with logic programming, miniKanren, or with writing interpreters or type inferencers. Some experience with functional programming, ideally in Scheme or Racket, would be useful but is not necessary.