A Typed Multi-level Datalog IR and Its Compiler Framework
David Klopp, Sebastian Erdweg, André Pacak
Abstract
The resurgence of Datalog in the last two decades has led to a multitude of new Datalog systems. These systems explore novel ideas for improving Datalog’s programmability and performance, making important contributions to the field. Unfortunately, the individual systems progress at a much slower pace than the overall field, because improvements in one system are rarely ported to other systems. The reason for this rift is that each system provides its own Datalog dialect with specific notation, language features, and invariants, enabling specific optimization and execution strategies. This paper presents the first compiler framework for Datalog that can be used to support any Datalog frontend language and to target any Datalog backend. The centerpiece of our framework is a novel typed multi-level Datalog IR that supports IR extensions and guarantees executability. Existing Datalog systems can provide a compiler frontend that translates their Datalog dialect to the extended IR. The IR is then progressively lowered toward core Datalog, allowing optimizations at each level. At last, compiler backends can target different Datalog solvers. We have implemented the compiler framework and integrated 4 Datalog frontends and 3 Datalog backends, using 16 IR extensions. We also formalize the IR’s flexible type system, which is bidirectional, flow-sensitive, bipolar, and uses three-valued typing contexts. The type system simultaneously validates type compatibility and precisely tracks bindings of logic variables while permitting IR extensions.
Ask about this paper
Your agent reads all of it.
Lune indexed this paper to the last equation, along with the top-tier papers that cite it. Ask a question and the answer quotes them.
Cited by top-tier papers1
Ask how each one uses itBuilds on7
- Incremental whole-program analysis in Datalog with latticesTamás Szabó, Sebastian Erdweg, Gábor BergmannPLDI 2021 · 39 citations
- Better Together: Unifying Datalog and Equality SaturationYihong Zhang, Yisu Remy Wang, Oliver Flatt, David Cao et al.PLDI 2023 · 38 citations
- Formulog: Datalog for SMT-based static analysisAaron Bembenek, Michael Greenberg, Stephen ChongOOPSLA 2020 · 26 citations
- Fixpoints for the masses: programming with first-class Datalog constraintsMagnus Madsen, Ondrej LhotákOOPSLA 2020 · 22 citations
- Rhombus: A New Spin on Macros without All the ParenthesesMatthew Flatt, Taylor Allred, Nia Angle, Stephen De Gabrielle et al.OOPSLA 2023 · 5 citations
Related papers
- A systematic approach to deriving incremental type checkersAndré Pacak, Sebastian Erdweg, Tamás SzabóOOPSLA 2020 · 16 citations
- Optimizing Parallel Recursive Datalog Evaluation on Multicore MachinesJiacheng Wu, Jin Wang, Carlo ZanioloSIGMOD 2022 · 9 citations
- Datalog with First-Class FactsThomas Gilray, Arash Sahebolamri, Yihao Sun, Sowmith Kunapaneni et al.VLDB 2025 · 3 citations
- Incremental Inference for Probabilistic DatalogXuyang Li, Weiyi Chen, Isil Dillig, Jingbo WangCAV 2026
- Interactive Debugging of Datalog ProgramsAndré Pacak, Sebastian ErdwegOOPSLA 2023 · 4 citations
