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 NovDisplayed time zone: Guadalajara, Mexico City, Monterrey change
10:30 - 12:00
|A Schematic Pushdown Reachability Language
|Domain-Specific Optimizations for Linear Pipelines