2025/11/01 by Igor Engel, Engel, Igor, Ekaterina Verbitskaia +1
Computer Science · #Advanced Software Engineering Methodologies #FOS: Computer and information sciences #Logic, programming, and type systems #Programming Languages (cs.PL) #Security and Verification in Computing
paper · pdf · doi:10.48550/arxiv.2511.00740
openalex publication_date 2025/11/01 · openalex created_date 2025/11/06 · openalex updated_date 2026/07/28
Relational programming enables program synthesis through a verifier-to-solver approach. An earlier paper introduced a functional conversion that mitigated some of the inherent performance overhead. However, the conversion was inelegant: it was oblivious to types, demanded determinism annotations, and implicit generator threading. In this paper, we address these issues by providing a typed tagless-final embedding of miniKanren into Haskell. This improvement significantly reduces boilerplate while preserving, and sometimes enhancing, earlier speedups.