sle2026/paper08

SLE 2026 paper:
A Shallow Embedding of Datalog in Lean

Ramy Shahin

• DOI: 10.1145/3806383.3815521
• arXiv preprint: 2605.02113
• Researchr: details/sle-2026/sle-2026/10/A-Shallow-Embedding-of-Datalog-in-Lean
• T1D: Composition
  • The main focus of the paper is on shallow embedding of one software language into another (Datalog and Lean), maximising interoperability.
• T3C: DSLs
  • Both Datalog and Lean are claimed to be domain-specific languages in the abstract.
• T5D: Formal Methods
  • Lean is a theorem prover / proof assistant, which puts it firmly into the formal methods field.
• T4C: Vertical Transformation
  • Datalog facts, rules, and queries are translated into native Lean constructs and proof terms.

---

The page is maintained by Dr. Vadim Zaytsev a.k.a. @grammarware. Last updated: July 2026.