Summer School on Relational Programming
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, 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.
Here are a few useful resources for the summer school. All of these resources, and much more are available on the miniKanren website:
I'd like for every student to implement miniKanren in a language of their choice during the summer school, since the core language is so small and easy to implement (about 60 lines in Scheme).
(an older talk, but quite gentle) Daniel P. Friedman and William E. Byrd. miniKanren "untalk" . Clojure/conj 2011, Raleigh, NC, November 10, 2011
(a recent talk showing interesting uses of relational programming) William Byrd. The Promise of Relational Programming . PolyConf 15, Poznań, Poland, 2 July 2015.
(shows how to implement a minimal relational language in ~60 lines of code) Jason Hemann and Daniel P. Friedman. microKanren: A Minimal Functional Core for Relational Programming . Proceedings of the 2013 Workshop on Scheme and Functional Programming (Scheme '13), Alexandria, VA, 2013. Complete source code (Scheme): https://github.com/jasonhemann/microKanren
(shows how to write a simple Scheme interpreter as a relation) William E. Byrd, Eric Holk, and Daniel P. Friedman. miniKanren, Live and Untagged: Quine Generation via Relational Interpreters (Programming Pearl) . Proceedings of the 2012 Workshop on Scheme and Functional Programming, Copenhagen, Denmark, 2012. Complete source code (Scheme): https://github.com/webyrd/2012-scheme-workshop-quines-paper-code
(details on the use and implementation of relational programming) William E. Byrd. Relational Programming in miniKanren: Techniques, Applications, and Implementations Implementations . Ph.D. thesis, Indiana University, Bloomington, IN, September 30, 2009.
- About schools
12-16 August 2019Summer School on Probabilistic Programming
27-31 August 2018Summer School on Category Theory
28 August - 1 September 2017Summer School on Weak Memory Consistency
30 January - 3 February 2017Winter School on Denotational Semantics
22-26 August 2016Summer School on Game Semantics
24-28 August 2015Summer School on Relational Programming
2-6 February 2015Winter School on Abstract Interpretation
25-29 August 2014Programs and Proofs: Mechanizing Mathematics with Dependent Types
3-7 February 2014Winter School on Metacalculations
26-30 August 2013Summer School on Memory Management