We show how easy it is to hook an SMT (Satisfiability Modulo Theory) solver such as CVC4 or Z3 as a backend to miniKanren, an embedded domain-specific language in Scheme, to create an environment for constraint logic programming. This combination inherits the best of both worlds: the high-level interleaved search and recursive unfolding of miniKanren, and the finely tuned low-level facilities of the underlying solver.
In this talk, we describe the simple implementation and illustrate the technology through interpreters, synthesis, symbolic execution / abstract interpretation, RSA, and music generation.
Tue 6 Nov
|10:30 - 11:00|
|11:00 - 11:30|
|11:30 - 12:00|