Pith. sign in

REVIEW 3 major objections 5 minor 114 references

Datalog with First-Class Facts

T0 review · 3 major / 5 minor · reviewed 2026-08-12 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read The paper introduces DL∃!, a Datalog variant in which every fact is identified by a unique Skolem term, and claims this single restriction makes tree-shaped data first-class while enabling a communication-avoiding, massively parallel…

desk verdict A genuinely new Datalog extension with a serious parallel implementation and strong benchmarks, but the formal semantics-to-engine connection is asserted, not demonstrated. read the letter →

arxiv 2411.14330 v2 pith:EOGHXDEY submitted 2024-11-21 cs.DB cs.PL

Thomas Gilray , Arash Sahebolamri , Yihao Sun , Sowmith Kunapaneni , Sidharth Kumar , Kristopher Micinski This is my paper · ORCID
classification cs.DBcs.PL
keywords Datalogfirst-classfactsSkolemtermsuniqueexistentialquantificationrestrictedchaseprovenanceabstractinterpretationdata-parallelrelationalalgebra
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

$\mathrm{DL}^{\exists!}$ is a restricted form of existential Datalog in which every deduced fact is assigned a unique symbolic identity, its Skolem term. The paper argues that this restriction makes tree-shaped data first-class: nested facts can trigger rules, be indexed, and be joined on their identities like ordinary tuples, without requiring unification. The authors build Slog, a distributed MPI engine that exploits the uniqueness restriction so that assigning fresh fact ids is a local, lock-free interning step. They report that Slog outperforms Nemo, VLog, RDFox, and Soufflé on eager why-provenance and control-flow-analysis benchmarks, and that a context-sensitive points-to analysis of Linux strong-scales from 16 to about 512 processes.

What carries the argument

The load-bearing object is the uniqueness restriction in rule heads: $\exists! id_H.\, id_H = H(\ldots)$ forbids the head identity from unifying with body variables or other head identities. This prevents cyclic fact construction, makes the satisfaction check in the restricted chase a pure membership test, and reduces deduplication to interning, where each new fact is stored in its canonical index and receives a 64-bit id split into relation, bucket, and local fact fields. The $\mathrm{DLS}$ surface language contributes a flattening translation that rewrites nested patterns into flat clauses plus explicit identity columns, so tree-shaped computation runs as ordinary relational joins over identities.

What would settle it

Take any terminating $\mathrm{DL}^{\exists!}$ program whose Herbrand intersection can be computed by hand, run Algorithm 1 to its fixed point, and compare the two sets: any fact produced by the chase but absent from the intersection, or any intersection fact the chase never produces, would refute Theorem H1.

Watch

Extended reading notes

Core claim

$\mathrm{DL}^{\exists!}$ extends Datalog with unique existential quantification in rule heads: each rule has the form $\exists! id_H.\, id_H = H(\ldots)$, so every generated fact is identified by a fresh Skolem term and identities cannot be unified with body variables. This syntactic restriction eliminates the need for unification: the restricted chase checks only whether the head tuple already exists, generates a fresh null when it does not, and thereby associates each (sub)fact with a unique intern id. On top of this, the paper defines $\mathrm{DLS}$, a surface language in which patterns can be written directly nested and are compiled to flat clauses with explicit identities via the translation in Figure 2. The paper claims that the least fixed point of the immediate consequence operator equals the model-theoretic denotation (Theorem H1), that Datalog programs embedded in $\mathrm{DL}^{\exists!}$ always terminate, and that the resulting engine Slog is data-parallel because fact identity assignment is just per-bucket deduplication and interning.

Load-bearing premise

The load-bearing premise is that the chase algorithm in Section 2.1 produces exactly the facts that the model-theoretic denotation specifies, a claim stated as Theorem H1 with only a citation to an Isabelle implementation that has no link or commit hash in this preprint.

Editorial extensions

If this is right

  • Nested, tree-shaped data such as abstract syntax trees, typing derivations, and derivation trees can be computed with standard relational joins and indexes; nested facts trigger rule evaluation instead of requiring a separate assertion step.
  • Eager why-provenance becomes practical: every derivation edge can be stored as a fact connecting body ids to head ids, making lineage a reachability query, and the paper reports speedups over on-demand systems on Galen, CSDA, Andersen, and transitive-closure workloads.
  • Program analyses that use first-class facts instead of algebraic data types avoid Cartesian-product scans; the compiled control-flow analyses show substantially better scaling than ADT-based evaluation as input size grows.
  • Because fresh fact ids are assigned locally per bucket, the fixed-point loop avoids global synchronization for identity generation, letting the MPI implementation strong-scale to around 512 processes on Linux-scale context-sensitive points-to analysis.
  • The Datalog fragment of $\mathrm{DL}^{\exists!}$ terminates, while full $\mathrm{DL}^{\exists!}$ is Turing-complete, so only programs that generate unboundedly many ids diverge.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • If the semantic equivalence holds, $\mathrm{DL}^{\exists!}$ could serve as a generic compile target for natural-deduction-style and functional-programming specifications, giving data-parallel engines access to workloads usually reserved for functional runtimes, such as type checkers and interpreters.
  • A testable extension would compare eager lineage in Slog against on-demand SAT-based why-provenance when only a few tuples need explanations; the paper's eager approach materializes all derivations, so the crossover point is an empirical question.
  • The fixed 64-bit id layout (16-bit relation, 16-bit bucket, 32-bit local) sets capacity limits per run; wider or variable-length ids would be a natural next step for very large distributed workloads.
  • Interning modulo a canonical form rather than syntactic identity would let Slog approximate equality-saturation reasoning while keeping lock-free parallel id assignment, connecting this work to equality-graph-based systems.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

3 major / 5 minor

Summary. The paper introduces DL∃!, a restriction of Datalog∃ in which every fact is identified by a Skolem term unique to the fact, and a surface language DLS with syntactically nested facts. The authors present a chase-based operational semantics, a fixed-point semantics, and a model-theoretic semantics for the language; they then describe Slog, an MPI-based parallel engine that compiles DLS to relational-algebra kernels, using a distributed interning phase to assign unique 64-bit fact identities. The paper demonstrates the language on why-provenance, algebraic-data-type encodings, functional-programming encodings, structural abstract interpretation, and type systems, and it reports performance comparisons against Nemo, VLog, RDFox, and Soufflé, plus strong-scaling results on the Theta supercomputer.

Significance. The design point is genuinely attractive: by forbidding unification of fact identities, tree-shaped data becomes first-class, indexable, and joinable in a way that ordinary Datalog and ADT-based extensions do not naturally provide. If the semantic claims hold, the work gives a practical and parallel-friendly compromise between flat Datalog and general Datalog∃. The evaluation is substantial and externally grounded: Table 1 compares Slog against three other engines on provenance workloads; Table 2 shows large performance gaps against Soufflé on CFA benchmarks; Figure 8 reports scaling to 2,048 processes. The paper also ships concrete applications (why-provenance, STLC, lambda-calculus interpreter, AAM-style CFA) that make the contribution easy to assess. I found no fitted parameters and no circular evaluation: the comparisons are against external systems. The main weakness is that the central semantic correctness claims are promised but not verifiable from the manuscript.

major comments (3)
  1. [§2.4–2.5, Theorem H1] The paper states 'we elide a detailed proof, but refer the reader to our Isabelle implementation' and marks Lemmas H1–H4 and Theorem H1 as formalized in Isabelle/HOL, yet no artifact link, repository path, or commit hash is supplied. The conclusion repeats that the equivalence is 'formally' proved in Isabelle/HOL. As written, the central correctness claim of the paper is not checkable from the preprint. Please provide a stable link to the Isabelle sources, state which statements are actually proved, and include at least a proof sketch for Theorem H1 in the paper itself.
  2. [§2.1 vs. §2.3] Algorithm 1 is presented as 'the semantics of DL∃!' and produces a stream of id-annotated facts of the form idH = H(...), while the fixed-point operator IC_P in Section 2.3 is defined over id-free structured Facts (Val ::= R(Val,...) | Lit). Theorem H1 only relates lfp(IC_P) to the model-theoretic denotation; there is no theorem stating that Algorithm 1's chase computes lfp(IC_P), no formal correspondence between fresh nulls and structural fact identities, and no proof that the frontier condition in Algorithm 1 (line 3, requiring phiθ ∩ Δ_i ≠ ∅) preserves the least fixed point under semi-naive evaluation. Since Slog's operational behavior is semi-naive evaluation of DLS rules, this missing bridge leaves the implemented engine formally disconnected from the claimed denotational meaning. This is load-bearing for both the language design and the benchmark claims; please add and prove the chase-to-fixed-point equivalence, or state and prove a precise approximation statement.
  3. [§2.2, Figure 2] The flatten translation from DLS to DL∃! is defined syntactically, and the introduction calls DLS 'equivalent in power' to DL∃!, but no theorem states that flatten preserves the fixed-point or model-theoretic semantics. Because Slog compiles DLS via this translation (Section 4), a correctness bug in flatten would disconnect the benchmarked implementation from the language's formal semantics. Please add a semantics-preservation lemma with a proof sketch, or explicitly include this result in the Isabelle formalization and verify it there.
minor comments (5)
  1. [§1, §6] There are several typos: 'parllelism' in the introduction, 'state-of-art' in contribution (4), 'wile' in Section 6, and 'V alues' in the Fact grammar in Section 2.3.
  2. [§2.4] The phrase 'any nontrivial DL∃! program' is used without a definition; for example, a program using only a zero-arity relation symbol has a finite Herbrand universe.
  3. [References] Reference [9] contains the placeholder string '#PLACEHOLDER_PARENT_METADATA_VALUE#' in the venue field; this should be corrected to the actual proceedings name.
  4. [§5.1, Table 1] The text says 'The first column of the table shows four selected Datalog queries,' but the first column contains benchmark/workload names such as Galen, CSDA, Andersen, and TC; please clarify the distinction between query and dataset.
  5. [§4.1] The intern-ID layout reserves 16 bits for relation ID, 16 bits for bucket ID, and 32 bits for a per-process fact ID; the paper does not discuss overflow behavior if a relation or bucket exceeds these bounds. A short remark on this implementation limit would be helpful.

Circularity Check

0 steps flagged · score 1.0 of 10

No significant circularity: the core DL∃! semantic and implementation claims are not definitionally tied to their own inputs; the main weakness is an unverifiable elided Isabelle proof, which is a correctness gap rather than a circular one.

full rationale

The derivation chain is self-contained with respect to the core language design. DL∃! is defined syntactically in Section 2.1, its chase semantics is given by Algorithm 1, the fixed-point semantics is defined in Section 2.3 via IC_P, and the model-theoretic semantics in Section 2.4 is the intersection of Herbrand models. Theorem H1 asserts equivalence between the model-theoretic and fixed-point semantics, but the proof is elided and deferred to an Isabelle implementation with no link or commit hash. That is a verifiability gap, not circularity: the theorem is not assumed as an input to the construction, and its statement is not definitionally identical to any earlier equation. The DLS flattening in Figure 2 is a syntax-directed translation anchored by subfact-closure, and the implementation evaluation compares against external systems (Nemo, VLog, RDFox, Soufflé) on external benchmarks, so no fitted parameter is renamed as a prediction. The authors reuse their prior BPRA parallel relational algebra infrastructure (references 44, 45, 62) and a prior all-to-all communication optimization (reference 37); these self-citations are implementation antecedents, not a uniqueness theorem or an ansatz smuggled in as an external necessity. The claimed benefit of the DL∃! restriction, namely avoiding unification and enabling lock-free interning, is argued from the language's own syntax and the chase definition rather than from the cited prior work. Consequently, no circular step can be pinned to a specific equation or citation, and the appropriate circularity score is low.

Assumptions & free parameters 1 free parameters · 5 assumptions · 1 invented entities

The central claim rests on the chase-based semantics, the syntactic restriction forbidding head-body identity unification, and the subfact-closure assumption. The formal equivalence proof is asserted rather than shown in the text. The intern ID layout is a hand-chosen numeric design parameter. No fitted model parameters are used.

free parameters (1)
  • Intern ID bit layout = 16-bit relation ID, 16-bit bucket ID, 32-bit unique ID
    Hand-chosen split of the 64-bit intern ID described in Section 4. It affects the maximum number of facts per bucket and scalability, but it is not fitted to benchmark outcomes.
assumptions (5)
  • standard math Tarski fixed-point theorem: a monotone operator over a complete lattice has a least fixed point.
    Used in Section 2.3 to define the least fixed point of the immediate consequence operator IC_P.
  • standard math Herbrand model intersection property: the set of all Herbrand models is closed under intersection.
    Lemma H2 in Section 2.4, needed to define the denotation of a program as the intersection of all Herbrand models.
  • domain assumption Head identities may not unify with body variables, which prevents cyclic fact construction.
    This syntactic restriction is the defining rule of DL∃! in Section 2.1 and is claimed to keep the chase free of cyclic facts.
  • domain assumption Every database is subfact-closed: every sub-fact of a fact is itself present.
    Assumed in Section 2.2 and Section 2.3 to make nested facts usable in joins and to define the subfact function.
  • domain assumption Non-termination of the chase occurs exactly when the program generates an unbounded number of ids.
    Stated in Section 2.1 without proof; it underlies the use of semi-naive evaluation and the termination discussion.
invented entities (1)
  • Unique Skolem fact identity / intern ID independent evidence
    purpose: Gives every fact a unique nested identity that can be joined upon and used in rule heads, enabling first-class tree-shaped facts and bucket-local deduplication.
    The construct is implemented in Slog and its behavior is observable in benchmarks; it is a semantic and implementation device, not a physical entity.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Datalog with First-Class Facts." pith.science (2026). https://pith.science/paper/EOGHXDEY

@misc{pith2026241114330,
  author       = {Pith},
  title        = {Pith review of: Datalog with First-Class Facts},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/EOGHXDEY}},
  note         = {Machine review of arXiv:2411.14330}
}
abstract

Datalog is a popular logic programming language for deductive reasoning tasks in a wide array of applications, including business analytics, program analysis, and ontological reasoning. However, Datalog's restriction to flat facts over atomic constants leads to challenges in working with tree-structured data, such as derivation trees or abstract syntax trees. To ameliorate Datalog's restrictions, popular extensions of Datalog support features such as existential quantification in rule heads (Datalog$^\pm$, Datalog$^\exists$) or algebraic data types (Souffl\'e). Unfortunately, these are imperfect solutions for reasoning over structured and recursive data types, with general existentials leading to complex implementations requiring unification, and ADTs unable to trigger rule evaluation and failing to support efficient indexing. We present DL$^{\exists!}$, a Datalog with first-class facts, wherein every fact is identified with a Skolem term unique to the fact. We show that this restriction offers an attractive price point for Datalog-based reasoning over tree-shaped data, demonstrating its application to databases, artificial intelligence, and programming languages. We implemented DL$^{\exists!}$ as a system \slog{}, which leverages the uniqueness restriction of DL$^{\exists!}$ to enable a communication-avoiding, massively-parallel implementation built on MPI. We show that Slog outperforms leading systems (Nemo, Vlog, RDFox, and Souffl\'e) on a variety of benchmarks, with the potential to scale to thousands of threads.

Figures

Figures reproduced from arXiv: 2411.14330 by the authors.

Figure 2
Figure 2. Compiling DLS into DL∃! respectively. DLS programs must also be well-scoped: variables ap￾pearing in a head clause must also be contained in the body; notice that DLS omits the existential quantification and assignment in the head, making the quantifier implicit. The definition of DLS is given via a syntax-directed translation given in [PITH_FULL_IMAGE:figures/full_fig_p003_2.png] view at source ↗
Figure 1
Figure 1. Syntax of DLS: R is a relation name. We now extend DL∃! to DLS, syntactic sugar on top of DL∃! which allows syntactically-nested facts and patterns, such as𝐺(𝐺(𝑥)). The syntax of DLS is shown in [PITH_FULL_IMAGE:figures/full_fig_p003_1.png] view at source ↗
Figure 3
Figure 3. Lambda-calculus interpreter (⇓) in DLS. (𝑥) to the argument value (𝑣𝑎) using a (↦→) fact. Finally, the top rule (shown parallel to App on the left) puts this all together and deduces that the application expression’s value is the same as that of the function body under the appropriate environment. IncA, the other recent approach to encoding functional program￾ming in Datalog [77, 78] requires static monomorphization… view at source ↗
Figures from the paper (5 more)
Figure 5
Figure 5. Figure 5: STLC type rules (left); equivalent DLS (right). DL∃! (see §4), and Soufflé (see §3.3). It is derived from a stack￾passing interpreter—a call-by-value Krivine’s machine [58]—with a store factored out [PITH_FULL_IMAGE:figures/full_fig_p007_5.png]
Figure 4
Figure 4. Figure 4: A global-store 𝑚-CFA—evaluated in [PITH_FULL_IMAGE:figures/full_fig_p007_4.png]
Figure 6
Figure 6. Figure 6: An illustration of the main phases of our parallel [PITH_FULL_IMAGE:figures/full_fig_p008_6.png]
Figure 7
Figure 7. Figure 7: Example C++ code generated by Soufflé [PITH_FULL_IMAGE:figures/full_fig_p010_7.png]
Figure 8
Figure 8. Figure 8: Scaling CSPA (of Linux) on Theta. with high iteration count and low per-iteration work. As problem size increases, our Slog implementations show healthy scalabil￾ity; efficiency grows as problem size grows (e.g., 24:10 to 6:45 on 15-𝑚-CFA/384, 22:46 to 7:28 on 12-𝑚-CFA…

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

114 extracted references · 56 canonical work pages

  1. [1]

    1995.Foundations of databases: the logical level

    Serge Abiteboul, Richard Hull, and Victor Vianu. 1995.Foundations of databases: the logical level. Addison-Wesley Longman Publishing Co., Inc

    1995

  2. [2]

    Luke Ong

    Mario Alvarez-Picallo, Alex Eyers-Taylor, Michael Peyton Jones, and C.-H. Luke Ong. 2019. Fixing Incremental Computation. In Programming Languages and Systems, Luís Caires (Ed.). Springer International Publishing, Cham, 525–552

    2019

  3. [3]

    Nada Amin and Tiark Rompf. 2017. Collapsing towers of interpreters. Proceed- ings of the ACM on Programming Languages 2, POPL (2017), 1–33

    2017

  4. [4]

    Michael Anderson, Shaden Smith, Narayanan Sundaram, Mihai Capotă, Zheguang Zhao, Subramanya Dulloor, Nadathur Satish, and Theodore L. Willke

  5. [5]

    Tony Antoniadis, Konstantinos Triantafyllou, and Yannis Smaragdakis. 2017. Porting DOOP to soufflé: a tale of inter-engine portability for datalog-based analyses. In Proceedings of the 6th ACM SIGPLAN International Workshop on State Of the Art in Program Analysis . ACM, 25–30

    2017

  6. [6]

    Molham Aref, Balder Ten Cate, Todd J Green, Benny Kimelfeld, Dan Olteanu, Emir Pasalic, Todd L Veldhuizen, and Geoffrey Washburn. 2015. Design and im- plementation of the LogicBlox system. In Proceedings of the 2015 ACM SIGMOD International Conference on Management of Data . 1371–1382

    2015

  7. [7]

    Jean-François Baget, Michel Leclère, Marie-Laure Mugnier, Swan Rocher, and Clément Sipieter. 2015. Graal: A toolkit for query answering with existential rules. In Rule Technologies: Foundations, Tools, and Applications: 9th Interna- tional Symposium, RuleML 2015, Berlin, Germany, August 2-5, 2015, Proceedings

    2015

  8. [8]

    Jean-François Baget, Michel Leclère, Marie-Laure Mugnier, and Eric Salvat. 2011. On rules with existential variables: Walking the decidability line. Artificial In- telligence 175, 9-10 (2011), 1620–1654

    2011

Show all 114 references
  1. [9]

    Teodoro Baldazzi, Luigi Bellomarini, and Emanuel Sallinger. 2023. Rea- soning over Financial Scenarios with the Vadalog System. In # PLACE- HOLDER_PARENT_METADATA_V ALUE#, Vol. 26. OpenProceedings. org, 782– 791

    2023

  2. [11]

    Luigi Bellomarini, Davide Benedetto, Matteo Brandetti, and Emanuel Sallinger

  3. [12]

    Pierre Bourhis, Marco Manna, Michael Morak, and Andreas Pieris. 2016. Guarded-based disjunctive tuple-generating dependencies. ACM Transactions on Database Systems (TODS) 41, 4 (2016), 1–45

    2016

  4. [13]

    Katharina Brandl, Sebastian Erdweg, Sven Keidel, and Nils Hansen. 2023. Modu- lar Abstract Definitional Interpreters for WebAssembly. InEuropean Conference on Object-Oriented Programming (ECOOP 2023)

    2023

  5. [14]

    Proceedings of the VLDB Endowment 15, 13 (2022), 3976–3988

    Exploiting the power of equality-generating dependencies in ontological reasoning. Proceedings of the VLDB Endowment 15, 13 (2022), 3976–3988

    2022

  6. [15]

    Bruck, , S

    J. Bruck, , S. Kipnis, E. Upfal, and D. Weathersby. 1997. Efficient algorithms for all-to-all communications in multiport message-passing systems. IEEE Transactions on Parallel and Distributed Systems 8, 11 (Nov 1997), 1143–1156. https://doi.org/10.1109/71.642949

    1997 doi

  7. [16]

    Mihai Budiu, Tej Chajed, Frank McSherry, Leonid Ryzhyk, and Val Tannen

  8. [17]

    Martin Bravenboer and Yannis Smaragdakis. 2009. Strictly declarative spec- ification of sophisticated points-to analyses. In Proceedings of the 24th ACM SIGPLAN conference on Object oriented programming systems languages and applications (Orlando, Florida, USA) (OOPSLA ’09). A...

    2009

  9. [18]

    Marco Calautti, Ester Livshits, Andreas Pieris, and Markus Schneider. 2024. The Complexity of Why-Provenance for Datalog Queries. Proc. ACM Manag. Data 2, 2, Article 83 (may 2024), 16 pages. https://doi.org/10.1145/3651146

    2024 doi

  10. [19]

    Marco Calautti, Ester Livshits, Andreas Pieris, and Markus Schneider. 2024. Computing the Why-Provenance for Datalog Queries via SAT Solvers. In Pro- ceedings of the AAAI Conference on Artificial Intelligence , Vol. 38. 10459–10466

    2024

  11. [20]

    Andrea Calì, Georg Gottlob, and Thomas Lukasiewicz. 2009. A general datalog- based framework for tractable query answering over ontologies. In Proceedings of the twenty-eighth ACM SIGMOD-SIGACT-SIGART symposium on Principles of database systems. 77–86

    2009

  12. [21]

    Peter Buneman, Sanjeev Khanna, and Tan Wang-Chiew. 2001. Why and where: A characterization of data provenance. In Database Theory—ICDT 2001: 8th International Conference London, UK, January 4–6, 2001 Proceedings 8 . Springer, 316–330

    2001

  13. [22]

    David Carral, Irina Dragoste, Markus Krötzsch, and Christian Lewe. 2019. Chas- ing sets: how to use existential rules for expressive reasoning. In Proceedings of the 28th International Joint Conference on Artificial Intelligence (Macao, China) (IJCAI’19). AAAI Press, 1624–1631

    2019

  14. [23]

    David Carral, Irina Dragoste, and Markus Krötzsch. 2017. Restricted Chase (Non)Termination for Existential Rules with Disjunctions. In Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence, IJCAI-17 . 922–928. https://doi.org/10.24963/ijcai.2017/128

    2017 doi

  15. [24]

    Stefano Ceri, Georg Gottlob, Letizia Tanca, et al. 1989. What you always wanted to know about Datalog(and never dared to ask). IEEE transactions on knowledge and data engineering 1, 1 (1989), 146–166

    1989

  16. [25]

    David Carral, Irina Dragoste, and Markus Krötzsch. 2017. Restricted Chase (Non) Termination for Existential Rules with Disjunctions.. In IJCAI. 922–928

    2017

  17. [26]

    Cognitect, Inc. [n.d.]. Datomic: A Distributed Deductive Database in Clojure. https://www.datomic.com/. accessed: 9-22-2024

    2024

  18. [27]

    Patrick Cousot. 1996. Abstract interpretation. ACM Computing Surveys (CSUR) 28, 2 (1996), 324–328

    1996

  19. [28]

    Patrick Cousot and Radhia Cousot. 1977. Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approxima- tion of Fixpoints. In Proceedings of the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (Los Angeles,...

    1977

  20. [29]

    James Cheney, Laura Chiticariu, Wang-Chiew Tan, et al. 2009. Provenance in databases: Why, how, and where. Foundations and Trends® in Databases 1, 4 (2009), 379–474

    2009

  21. [30]

    Yingwei Cui and Jennifer Widom. 2000. Lineage tracing in a data warehousing system. In Proceedings of 16th International Conference on Data Engineering (Cat. No. 00CB37073). IEEE, 683–684

    2000

  22. [31]

    Yingwei Cui, Jennifer Widom, and Janet L. Wiener. 2000. Tracing the lineage of view data in a warehousing environment. ACM Trans. Database Syst. 25, 2 (jun 2000), 179–227. https://doi.org/10.1145/357775.357777

    2000

  23. [32]

    David Darais, Nicholas Labich, Phúc C Nguyen, and David Van Horn. 2017. Abstracting definitional interpreters (functional pearl). Proceedings of the ACM on Programming Languages 1, ICFP (2017), 1–25

    2017

  24. [33]

    Patrick Cousot and Radhia Cousot. 1979. Systematic design of program analysis frameworks. In Proceedings of the 6th ACM SIGACT-SIGPLAN symposium on Principles of programming languages . 269–282

    1979

  25. [34]

    Ali Elhalawati, Markus Krötzsch, and Stephan Mennicke. 2022. An existential rule framework for computing why-provenance on-demand for datalog. In International Joint Conference on Rules and Reasoning . Springer, 146–163

    2022

  26. [35]

    1985.Neat explanation of proof trees

    Agneta Eriksson and Anna-Lena Johansson. 1985.Neat explanation of proof trees. Uppsala University, Computing Science Department, Uppsala Programming

    1985

  27. [36]

    Javier Esparza, Michael Luttenberger, and Maximilian Schlund. 2015. Fpsolve: A generic solver for fixpoint equations over semirings. International Journal of Foundations of Computer Science 26, 07 (2015), 805–825

    2015

  28. [37]

    Davis and Yifan Hu

    Timothy A. Davis and Yifan Hu. 2011. The University of Florida Sparse Ma- trix Collection. ACM Trans. Math. Softw. 38, 1, Article 1 (dec 2011), 25 pages. https://doi.org/10.1145/2049662.2049663

    2011

  29. [38]

    Zhiwei Fan, Jianqiao Zhu, Zuyu Zhang, Aws Albarghouthi, Paraschos Koutris, and Jignesh Patel. 2018. Scaling-up in-memory datalog processing: Observations and techniques. arXiv preprint arXiv:1812.03975 (2018)

    2018 arXiv

  30. [39]

    Gérard Ferrand, Willy Lesaint, and Alexandre Tessier. 2005. Explanations and proof trees. In International Symposium on Explanation-A ware Computing, ExaCt

    2005

  31. [40]

    Message P Forum. 1994. MPI: A message-passing interface standard

    1994

  32. [41]

    Ke Fan, Thomas Gilray, Valerio Pascucci, Xuan Huang, Kristopher Micinski, and Sidharth Kumar. 2022. Optimizing the Bruck Algorithm for Non-Uniform All-to-All Communication. In Proceedings of the 31st International Symposium on High-Performance Parallel and Distributed Computin...

    2022

  33. [42]

    Kimball Germane and Jay McCarthy. 2021. Newly-single and loving it: improv- ing higher-order must-alias analysis with heap fragments. Proceedings of the ACM on Programming Languages 5, ICFP (2021), 1–28

    2021

  34. [43]

    Adams, and Matthew Might

    Thomas Gilray, Michael D. Adams, and Matthew Might. 2016. Allocation Char- acterizes Polyvariance: A Unified Methodology for Polyvariant Control-flow Analysis. In Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming (Nara, Japan) (ICFP ’16). A...

    2016

  35. [44]

    Thomas Gilray and Sidharth Kumar. 2019. Distributed Relational Algebra at Scale. In 2019 IEEE 26th International Conference on High Performance Computing, Data, and Analytics (HiPC). 12–22. https://doi.org/10.1109/HiPC.2019.00014

    2019

  36. [45]

    Kimball Germane and Michael D Adams. 2020. Liberate Abstract Garbage Collection from the Stack by Decomposing the Heap. In European Symposium on Programming. Springer, Cham, 197–223

    2020

  37. [46]

    Adams, Matthew Might, and David Van Horn

    Thomas Gilray, Steven Lyde, Michael D. Adams, Matthew Might, and David Van Horn. 2016. Pushdown Control-flow Analysis for Free. InProceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (St. Petersburg, FL, USA) (POPL ’16). ACM, New Y...

    2016

  38. [47]

    Green, Grigoris Karvounarakis, and Val Tannen

    Todd J. Green, Grigoris Karvounarakis, and Val Tannen. 2007. Provenance semirings. In Proceedings of the Twenty-Sixth ACM SIGMOD-SIGACT-SIGART Symposium on Principles of Database Systems (, Beijing, China,) (PODS ’07) . Association for Computing Machinery, New York, NY, USA, 3...

    2007

  39. [48]

    Jiaqi Gu, Yugo H Watanabe, William A Mazza, Alexander Shkapsky, Mohan Yang, Ling Ding, and Carlo Zaniolo. 2019. RaSQL: Greater power and per- formance for big data analytics with recursive-aggregate-SQL on Spark. In Proceedings of the 2019 International Conference on Managemen...

    2019

  40. [49]

    Thomas Gilray, Sidharth Kumar, and Kristopher Micinski. 2021. Compil- ing Data-Parallel Datalog. In Proceedings of the 30th ACM SIGPLAN Interna- tional Conference on Compiler Construction (Virtual, Republic of Korea) (CC 2021). Association for Computing Machinery, New York, NY...

    2021

  41. [50]

    Matthew Hennessy. 1990. The semantics of programming languages: an elemen- tary introduction using structural operational semantics . John Wiley & Sons, Inc

    1990

  42. [51]

    Alex Ivliev, Stefan Ellmauthaler, Lukas Gerlach, Maximilian Marx, Matthias Meißner, Simon Meusel, and Markus Krötzsch. 2023. Nemo: First glimpse of a new rule engine. arXiv preprint arXiv:2308.15897 (2023)

    2023 arXiv

  43. [52]

    Herbert Jordan, Bernhard Scholz, and Pavle Subotić. 2016. Soufflé: On synthesis of program analyzers. In Computer Aided Verification: 28th International Con- ference, CA V 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part II 28 , Swarat Chaudhuri and Azadeh Farzan...

    2016

  44. [53]

    Daniel Halperin, Victor Teixeira de Almeida, Lee Lee Choo, Shumo Chu, Paraschos Koutris, Dominik Moritz, Jennifer Ortiz, Vaspol Ruamviboonsuk, Jingjing Wang, Andrew Whitaker, Shengliang Xu, Magdalena Balazinska, Bill Howe, and Dan Suciu. 2014. Demonstration of the Myria Big Da...

    2014

  45. [54]

    Herbert Jordan, Pavle Subotić, David Zhao, and Bernhard Scholz. 2019. A spe- cialized B-tree for concurrent datalog evaluation. In Proceedings of the 24th symposium on principles and practice of parallel programming (Washington, District of Columbia) (PPoPP ’19). ACM, New York...

    2019

  46. [55]

    Gilles Kahn. 1987. Natural semantics. InAnnual symposium on theoretical aspects of computer science. Springer, 22–39

    1987

  47. [56]

    Yevgeny Kazakov, Markus Krötzsch, and František Simančík. 2014. The Incredi- ble ELK: From Polynomial Procedures to Efficient Reasoning with EL Ontologies. Journal of automated reasoning 53, 1 (2014), 1–61

    2014

  48. [57]

    Herbert Jordan, Pavle Subotić, David Zhao, and Bernhard Scholz. 2019. Brie: A specialized trie for concurrent datalog. In Proceedings of the 10th International Workshop on Programming Models and Applications for Multicores and Manycores (Washington, DC, USA) (PMAM’19). ACM, Ne...

    2019

  49. [58]

    Jean-Louis Krivine. 2007. A call-by-name lambda-calculus machine. Higher- order and symbolic computation 20, 3 (2007), 199–207

    2007

  50. [59]

    Deepa S Kumar and M Abdul Rahman. 2017. Performance Evaluation of Apache Spark Vs MPI: A Practical Case Study on Twitter Sentiment Analysis. Journal of Computer Science 13, 12 (Dec 2017), 781–794. https://doi.org/10.3844/jcssp. 2017.781.794

    2017 doi

  51. [60]

    Kumar, A

    R. Kumar, A. Mamidala, and D. K. Panda. 2008. Scaling alltoall collective on multi-core systems. In 2008 IEEE International Symposium on Parallel and Dis- tributed Processing. 1–8

    2008

  52. [61]

    Keep and R

    Andrew W. Keep and R. Kent Dybvig. 2013. A Nanopass Framework for Com- mercial Compiler Development. In Proceedings of the 18th ACM SIGPLAN Inter- national Conference on Functional Programming (Boston, Massachusetts, USA) (ICFP ’13). Association for Computing Machinery, New Yo...

    2013

  53. [62]

    Sidharth Kumar and Thomas Gilray. 2020. Load-balancing parallel relational algebra. In High Performance Computing: 35th International Conference, ISC High Performance 2020, Frankfurt/Main, Germany, June 22–25, 2020, Proceedings 35 . Springer, 288–308

    2020

  54. [63]

    Nicola Leone, Marco Manna, Giorgio Terracina, and Pierfrancesco Veltri. 2012. Efficiently computable Datalog∃ programs. In Thirteenth international confer- ence on the principles of knowledge representation and reasoning

    2012

  55. [64]

    David Maier, Alberto O Mendelzon, and Yehoshua Sagiv. 1979. Testing implica- tions of data dependencies. ACM Transactions on Database Systems (TODS) 4, 4 (1979), 455–469

    1979

  56. [65]

    Schmidt, Peer-Timo Bremer, Eric Brugger, Venkatram Vishwanath, Philip Carns, Hemanth Kolla, Ray Grout, Jacqueline Chen, Martin Berzins, Giorgio Scorzelli, and Valerio Pascucci

    Sidharth Kumar, Cameron Christensen, JohnA. Schmidt, Peer-Timo Bremer, Eric Brugger, Venkatram Vishwanath, Philip Carns, Hemanth Kolla, Ray Grout, Jacqueline Chen, Martin Berzins, Giorgio Scorzelli, and Valerio Pascucci. 2014. Fast Multiresolution Reads of Massive Simulation D...

    2014 doi

  57. [66]

    Frank McSherry, Derek Gordon Murray, Rebecca Isaacs, and Michael Isard. 2013. Differential dataflow.. In CIDR

    2013

  58. [67]

    Matthew Might. 2010. Abstract interpreters for free. In International Static Analysis Symposium (SAS ’10). Springer, 407–421

    2010

  59. [68]

    Matthew Might and Panagiotis Manolios. 2009. A posteriori soundness for non- deterministic abstract interpretations. In International Workshop on Verification, Model Checking, and Abstract Interpretation . Springer, 260–274

    2009

  60. [69]

    Per Martin-Löf. 1996. On the Meanings of the Logical Constants and the Justifi- cations of the Logical Laws. Nordic Journal of Philosophical Logic 1, 1 (1996), 11–60

    1996

  61. [70]

    Matthew Might, Yannis Smaragdakis, and David Van Horn. 2010. Resolving and exploiting the k-CFA paradox: illuminating functional vs. object-oriented program analysis. In Proceedings of the 31st ACM SIGPLAN Conference on Pro- gramming Language Design and Implementation . 305–315

    2010

  62. [71]

    Boris Motik, Yavor Nenov, Robert Piro, and Ian Horrocks. 2019. Maintenance of datalog materialisations revisited. Artificial Intelligence 269 (2019), 76–136

    2019

  63. [72]

    Boris Motik, Yavor Nenov, Robert Piro, Ian Horrocks, and Dan Olteanu. 2014. Parallel materialisation of datalog programs in centralised, main-memory RDF systems. In Proceedings of the AAAI Conference on Artificial Intelligence , Vol. 28

    2014

  64. [73]

    Matthew Might and Olin Shivers. 2008. Exploiting reachability and cardinality in higher-order flow analysis. Journal of Functional Programming 18, 5-6 (2008), 821–864

    2008

  65. [74]

    Yavor Nenov, Robert Piro, Boris Motik, Ian Horrocks, Zhe Wu, and Jay Banerjee

  66. [75]

    Phuc C Nguyen, Thomas Gilray, Sam Tobin-Hochstadt, and David Van Horn

  67. [76]

    André Pacak and Sebastian Erdweg. 2019. Generating incremental type services. In Proceedings of the 12th ACM SIGPLAN International Conference on Software Language Engineering (Athens, Greece) (SLE 2019). Association for Computing Machinery, New York, NY, USA, 197–201. https://...

    2019 doi

  68. [77]

    Derek G Murray, Frank McSherry, Rebecca Isaacs, Michael Isard, Paul Barham, and Martín Abadi. 2013. Naiad: a timely dataflow system. In Proceedings of the Twenty-Fourth ACM Symposium on Operating Systems Principles . 439–455

    2013

  69. [78]

    André Pacak, Sebastian Erdweg, and Tamás Szabó. 2020. A systematic approach to deriving incremental type checkers. Proc. ACM Program. Lang. 4, OOPSLA, Article 127 (Nov. 2020), 28 pages. https://doi.org/10.1145/3428195

    2020 doi

  70. [79]

    Scott Parker, Vitali Morozov, Sudheer Chunduri, Kevin Harms, Chris Knight, and Kalyan Kumaran. 2017. Early Evaluation of the Cray XC40 Xeon Phi System ‘Theta’at Argonne. Technical Report. Argonne National Lab.(ANL), Argonne, IL (United States)

    2017

  71. [80]

    Benjamin C. Pierce. 2002. Types and Programming Languages (1st ed.). The MIT Press

    2002

  72. [81]

    Proceedings of the ACM on Programming Languages 2, POPL (2017), 51

    Soft contract verification for higher-order stateful programs. Proceedings of the ACM on Programming Languages 2, POPL (2017), 51

    2017

  73. [82]

    Gordon D Plotkin. 1981. Structural operational semantics. Aarhus University, Denmark (1981), 20–23

    1981

  74. [83]

    André Pacak and Sebastian Erdweg. 2022. Functional programming with Data- log. In 36th European Conference on Object-Oriented Programming (ECOOP 2022) . Schloss Dagstuhl-Leibniz-Zentrum für Informatik

    2022

  75. [84]

    John C Reynolds. 1972. Definitional interpreters for higher-order programming languages. In Proceedings of the ACM annual conference-Volume 2 . 717–740

    1972

  76. [85]

    Arash Sahebolamri, Langston Barrett, Scott Moore, and Kristopher Micinski

  77. [86]

    David S Scott. 1991. Efficient all-to-all communication patterns in hypercube and mesh topologies. In The Sixth Distributed Memory Computing Conference,

    1991

  78. [87]

    Benjamin C. Pierce. 2004. Advanced Topics in Types and Programming Languages. The MIT Press

    2004

  79. [88]

    Jiwon Seo, Jongsoo Park, Jaeho Shin, and Monica S. Lam. 2013. Distributed So- cialite: A Datalog-Based Language for Large-Scale Graph Analysis. Proc. VLDB Endow. 6, 14 (sep 2013), 1906–1917. https://doi.org/10.14778/2556549.2556572

    2013

  80. [89]

    Reyes-Ortiz, Luca Oneto, and Davide Anguita

    Jorge L. Reyes-Ortiz, Luca Oneto, and Davide Anguita. 2015. Big Data Analytics in the Cloud: Spark on Hadoop vs MPI/OpenMP on Beowulf.Procedia Computer Science 53 (2015), 121–130. https://doi.org/10.1016/j.procs.2015.07.286 INNS Conference on Big Data 2015 Program San Francisc...

    2015 doi

  81. [90]

    Olin Shivers. 1991. Control-Flow Analysis of Higher-Order Languages . Ph.D. Dissertation. Carnegie-Mellon University, Pittsburgh, PA

    1991

  82. [91]

    Alexander Shkapsky, Mohan Yang, Matteo Interlandi, Hsuan Chiu, Tyson Condie, and Carlo Zaniolo. 2016. Big Data Analytics with Datalog Queries on Spark. In Proceedings of the 2016 International Conference on Management of Data (San Francisco, California, USA)(SIGMOD ’16). Assoc...

    2016 doi

  83. [92]

    Bring Your Own Data Structures to Datalog. Proc. ACM Program. Lang. 7, OOPSLA2, Article 264 (oct 2023), 26 pages. https://doi.org/10.1145/3622840

    2023 doi

  84. [93]

    Robert Tarjan. 1972. Depth-first search and linear graph algorithms. SIAM journal on computing 1, 2 (1972), 146–160

    1972

  85. [94]

    Alfred Tarski. 1955. A lattice-theoretical fixpoint theorem and its applications. Pacific journal of Mathematics 5, 2 (1955), 285–309

    1955

  86. [95]

    Jiwon Seo, Stephen Guo, and Monica S Lam. 2013. SociaLite: Datalog extensions for efficient social network analysis. In 2013 IEEE 29th International Conference on Data Engineering (ICDE) . IEEE, 278–289

    2013

  87. [96]

    Sam Tobin-Hochstadt and David Van Horn. 2012. Higher-order symbolic execu- tion via contracts. In Proceedings of the ACM international conference on Object oriented programming systems languages and applications . 537–554

    2012

  88. [97]

    Ilya Sergey, Dominique Devriese, Matthew Might, Jan Midtgaard, David Darais, Dave Clarke, and Frank Piessens. 2013. Monadic abstract interpreters. In Pro- ceedings of the 34th ACM SIGPLAN conference on Programming language design and implementation. 399–410

    2013

  89. [98]

    Jacopo Urbani, Ceriel Jacobs, and Markus Krötzsch. 2016. Column-oriented datalog materialization for large knowledge graphs. In Proceedings of the AAAI Conference on Artificial Intelligence, Vol. 30

    2016

  90. [99]

    Patrick Valduriez and Setrag Khoshafian. 1988. Parallel Evaluation of the Tran- sitive Closure of a Database Relation. Int. J. Parallel Program. 17, 1 (Feb. 1988), 19–42

    1988

  91. [100]

    Yihao Sun, Ahmedur Rahman Shovon, Thomas Gilray, Kristopher Micinski, and Sidharth Kumar. 2023. GDlog: A GPU-Accelerated Deductive Engine. arXiv:2311.02206 [cs.DB]

    2023 arXiv

  92. [101]

    Kai Wang, Aftab Hussain, Zhiqiang Zuo, Guoqing Harry Xu, and Ardalan Amiri Sani. 2017. Graspan: A Single-machine Disk-based Graph System for Inter- procedural Static Analyses of Large-scale Systems Code. Proceedings of the Twenty-Second International Conference on Architectura...

    2017

  93. [102]

    Guannan Wei, Yuxuan Chen, and Tiark Rompf. 2019. Staged abstract inter- preters: Fast and modular whole-program analysis via meta-programming. Proceedings of the ACM on Programming Languages 3, OOPSLA (2019), 1–32

    2019

  94. [103]

    Rajeev Thakur, Rolf Rabenseifner, and William Gropp. 2005. Optimization of Collective Communication Operations in MPICH. Int. J. High Perform. Comput. Appl. 19, 1 (Feb. 2005), 49–66

    2005

  95. [104]

    Max Willsey, Chandrakana Nandi, Yisu Remy Wang, Oliver Flatt, Zachary Tatlock, and Pavel Panchekha. 2021. Egg: Fast and Extensible Equality Sat- uration. Proc. ACM Program. Lang. 5, POPL, Article 23 (jan 2021), 29 pages. https://doi.org/10.1145/3434304

    2021 doi

  96. [105]

    Jesper Larsson Träff, Antoine Rougier, and Sascha Hunold. 2014. Implementing a classic: Zero-copy all-to-all communication with MPI datatypes. InProceedings of the 28th ACM international conference on Supercomputing . 135–144

    2014

  97. [106]

    Yihong Zhang, Yisu Remy Wang, Max Willsey, and Zachary Tatlock. 2022. Re- lational e-matching. Proc. ACM Program. Lang. 6, POPL, Article 35 (jan 2022), 22 pages. https://doi.org/10.1145/3498696

    2022 doi

  98. [107]

    C. Zhao, Z. Zhang, P. Xu, T. Zheng, and J. Guo. 2020. Kaleido: An Efficient Out-of-core Graph Mining System on A Single Machine. In 2020 IEEE 36th International Conference on Data Engineering (ICDE) . 673–684

    2020

  99. [108]

    David Van Horn and Matthew Might. 2010. Abstracting Abstract Machines. In Proceedings of the 15th ACM SIGPLAN International Conference on Functional Programming (Baltimore, Maryland, USA) (ICFP ’10). ACM, New York, NY, USA, 51–62. https://doi.org/10.1145/1863543.1863553

    2010

  100. [111]

    Guannan Wei, James Decker, and Tiark Rompf. 2018. Refunctionalization of ab- stract abstract machines: bridging the gap between abstract abstract machines and abstract definitional interpreters (functional pearl). Proceedings of the ACM on Programming Languages 2, ICFP (2018), 1–28

    2018

  101. [113]

    Rohit Zambre, Damodar Sahasrabudhe, Hui Zhou, Martin Berzins, Aparna Chandramowlishwaran, and Pavan Balaji. 2021. Logically Parallel Communi- cation for Fast MPI+ Threads Applications. IEEE Transactions on Parallel and Distributed Systems (2021)

    2021

  102. [1991]

    IEEE Computer Society, 398–399

    Proceedings. IEEE Computer Society, 398–399

  103. [2015]

    RDFox: A Highly-Scalable RDF Store. In The Semantic Web - ISWC 2015 , Marcelo Arenas, Oscar Corcho, Elena Simperl, Markus Strohmaier, Mathieu d’Aquin, Kavitha Srinivas, Paul Groth, Michel Dumontier, Jeff Heflin, Krish- naprasad Thirunarayan, and Steffen Staab (Eds.). Springer ...

    2015

  104. [2017]

    Bridging the Gap between HPC and Big Data Frameworks. Proc. VLDB Endow. 10, 8 (apr 2017), 901–912. https://doi.org/10.14778/3090163.3090168

    2017

  105. [2022]

    Exploiting the Power of Equality-Generating Dependencies in Onto- logical Reasoning. Proc. VLDB Endow. 15, 13 (Sept. 2022), 3976–3988. https: //doi.org/10.14778/3565838.3565850

    2022

  106. [2023]

    DBSP: Automatic Incremental View Maintenance for Rich Query Lan- guages. Proc. VLDB Endow. 16, 7 (mar 2023), 1601–1614. https://doi.org/10. 14778/3587136.3587137

    2023

Pith tools

Reviewed August 12, 2026 · model on record in the stance chip above.