Resources from the Polyconf 2015 talk & relational interpreters workshop
Scheme Racket
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Failed to load latest commit information.


Resources from both the PolyConf 2015 talk and relational interpreters workshop

PolyConf 2015:


append, appendo, proof checker/theorem prover code: talk-code/scheme-interpreter/poly-scheme.scm

Semantics for the WHILE language adapted from 'Semantics with Applications: A Formal Introduction' by Hanne Riis Nielson and Flemming Nielson. Wiley Professional Computing, (240 pages, ISBN 0 471 92980 8), Wiley, 1992. Revised 1999 version available online at:

Symbolic execution example adapted from Stephen Chong's slides (with content from slides by Jeff Foster):

Symbolic execution code in WHILE: talk-code/while-interpreter/poly-while.scm

Example symbolic execution call: talk-code/while-interpreter/poly-trans.scm


Write a Relational Scheme Interpreter in miniKanren

This workshop will cover the fundamentals of programming in miniKanren, an embedded domain specific language for constraint logic programming. We will begin with an overview of the miniKanren language, and will write a few simple miniKanren relations that "run backward." We will then write a more sophisticated miniKanren program: an environment-passing Scheme interpreter, written as a relation. We will extend the interpreter in various ways, and explore how the interpreter can be used for program synthesis.

Minimal Scheme/Call-by-Value Lambda-calculus interpreter, written in Scheme: workshop-code/interp.scm

Minimal Scheme/Call-by-Value Lambda-calculus interpreter, written in miniKanren: workshop-code/interpo.scm

Transcripts from the workshop: workshop-code/trans.scm, workshop-code/trans2.scm

Faster miniKanren implementation (Racket and Vicare Scheme):


Vicare Scheme:

Veneer (client-side JavaScript compiler for miniKanren):