arXiv subjects

Dmitry Boulytchev

Publications and source records attributed to Dmitry Boulytchev.

9 recordsLinked to original sources

arXiv2026

Efficient Rational Unification for miniKanren

We present an efficient algorithm for rational term unification in persistent settings which demonstrates a comparable performance w.r.t. the conventional miniKanren unification with triangular substitution for Herbrand terms. Our algorithm is based on existing Martelli-Rossi approach and uses some adjustments to make the implementation more conventional. We provide certified proofs of principal algorithm properties in the Rocq proof assistant and showcase the results of a comprehensive performance evaluation.

cs.LO↗

arXiv2025

An Empirical Study of Rational Tree Unification for miniKanren

We present a study of unification for rational trees in the context of miniKanren. We give the definition of rational trees, specify the unification algorithm and prove some of its properties. We also introduce a number of heuristic optimizations and evaluate them for a number of relevant benchmarks. Finally we discuss the relations between rational and conventional unification algorithms and possible scenarios of their coexistence in the context of relational programming.

cs.LO↗

arXiv2024

A Relational Solver for Constraint-based Type Inference

We present a miniKanren-based type inferencer for an educational programming language with first-class functions, S-expressions, and pattern-matching. The language itself is untyped which adds a certain specificity to the problem and requires the employment of techniques conventionally used in implicit/gradual typing settings. The presence of polymorphic and recursive types poses a certain challenge when implementing the inferencer in miniKanren and requires a number of tricks, optimizations, and extensions to be used; we report on those as well.

cs.PL↗

arXiv2022

Reimplementing the Wheel: Teaching Compilers with a Small Self-Contained One

We report on a one-semester compiler construction course based on the idea of implementing a small self-contained compiler for a small model language from scratch, not using other compiler construction frameworks. The course is built around an evolving family of languages with increasing expressiveness and complexity, which finally is crowned by a language with first-class functions, S-expressions, pattern matching, and garbage collection. The code generation technique is based on the idea of symbolic interpreters, which allows to implement a robust albeit not a very efficient native code generator. We give the motivation for the course, describe its structure, and report some results of teaching based on students' post-course surveys.

cs.PL↗

arXiv2022

Scheduling Complexity of Interleaving Search

miniKanren is a lightweight embedded language for logic and relational programming. Many of its useful features come from a distinctive search strategy, called interleaving search. However, with interleaving search conventional ways of reasoning about the complexity and performance of logical programs become irrelevant. We identify an important key component -- scheduling -- which makes the reasoning for miniKanren so different, and present a semi-automatic technique to estimate the scheduling impact via symbolic execution for a reasonably wide class of programs.

cs.PL↗

arXiv2021

An Empirical Study of Partial Deduction for miniKanren

We study conjunctive partial deduction, an advanced specialization technique aimed at improving the performance of logic programs, in the context of relational programming language miniKanren. We identify a number of issues, caused by miniKanren peculiarities, and describe a novel approach to specialization based on partial deduction and supercompilation. The results of the evaluation demonstrate successful specialization of relational interpreters. Although the project is at an early stage, we consider it as the first step towards an efficient optimization framework for miniKanren.

cs.PL↗

arXiv2021

Generic Programming with Combinators and Objects

We present a generic programming framework for OCAML which makes it possible to implement extensible transformations for a large scale of type definitions. Our framework makes use of objectoriented features of OCAML, utilising late binding to override the default behaviour of generated transformations. The support for polymorphic variant types complements the ability to describe composable data types with the ability to implement composable transformations.

cs.PL↗

arXiv2020

Certified Semantics for Relational Programming

We present a formal study of semantics for the relational programming language miniKanren. First, we formulate a denotational semantics which corresponds to the minimal Herbrand model for definite logic programs. Second, we present operational semantics which models interleaving, the distinctive feature of miniKanren implementation, and prove its soundness and completeness w.r.t. the denotational semantics. Our development is supported by a Coq specification, from which a reference interpreter can be extracted. We also derive from our main result a certified semantics (and a reference interpreter) for SLD resolution with cut and prove its soundness.

cs.PL↗

arXiv2018

Typed Embedding of a Relational Language in OCaml

We present an implementation of the relational programming language miniKanren as a set of combinators and syntax extensions for OCaml. The key feature of our approach is polymorphic unification, which can be used to unify data structures of arbitrary types. In addition we provide a useful generic programming pattern to systematically develop relational specifications in a typed manner, and address the problem of integration of relational subsystems into functional applications.

cs.PL↗