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.

Conference Day
Thu 22 Aug

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

10:30 - 12:00
Session 2miniKanren at Elk
Chair(s): Lisa ZhangUniversity of Toronto
10:30
45m
Full-paper
Relational Interpreters for Search Problems
miniKanren
Petr LozovSain Petersburg State University, SPbGU, Ekaterina VerbitskaiaSaint Petersburg State University, Russia, Dmitri Boulytchev
Link to publication
11:15
45m
Full-paper
Relational Processing for Fun and Diversity: Simulating a CPU relationally with miniKanren
miniKanren
Gilmore R. Lundquist, Utsav Bhatt, Kevin HamlenUniversity of Texas at Dallas, USA
Link to publication