miniKanren is a domain-specific language for relational programming, in which programs are modeled as mathematical relations; these relations make no distinction between inputs and outputs. miniKanren can be thought of as a purely declarative constraint logic programming language, implemented as a combination of search and constraint solving. An appealing aspect of relational programming is that operational semantics, typing judgments, rewriting rules, and other formal semantics are commonly written as relations; these semantics can often be expressed directly in miniKanren, with a minimum of translation. Once these semantics are encoded as miniKanren relations, miniKanren’s search and constraint solving allows these semantics to be used for synthesis. For example, encoding the operational semantics for a subset of Scheme in miniKanren allows us to synthesize recursive Scheme programs. In this talk I’ll demonstrate how to encode several types of semantics in miniKanren, and show how programs and expressions can be synthesized from these executable semantics.