Write a Blog >>
ICFP 2019
Sun 18 - Fri 23 August 2019 Berlin, Germany
Thu 22 Aug 2019 10:30 - 11:15 at Elk - Session 2 Chair(s): Lisa Zhang

We address the problem of constructing a solver for a certain search problem from its solution verifier. The main idea behind the approach we advocate is to consider a verifier as an interpreter which takes a data structure to search in as a program and a candidate solution as this program’s input. As a result the interpreter returns “true” if the candidate solution satisfies all constraints and “false” otherwise. Being implemented in a relational language, a verifier becomes capable of finding a solution as well. We apply two techniques to make this scenario realistic: relational conversion and supercompilation. Relational conversion makes it possible to convert a first-order functional program into relational form, while supercompilation (in the form of conjunctive partial deduction (CPD)) — to optimize out redundant computations. We demonstrate our approach on a number of examples using a prototype tool for OCanren — an implementation of miniKanren for OCaml, — and discuss the results of evaluation.

Thu 22 Aug

10:30 - 12:00: miniKanren 2019 - Session 2 at Elk
Chair(s): Lisa ZhangUniversity of Toronto
minikanren-2019-papers10:30 - 11:15
Petr LozovSain Petersburg State University, SPbGU, Ekaterina VerbitskaiaSaint Petersburg State University, Russia, Dmitri Boulytchev
Link to publication
minikanren-2019-papers11:15 - 12:00
Gilmore R. Lundquist, Utsav Bhatt, Kevin HamlenUniversity of Texas at Dallas, USA
Link to publication