20 citations · 27 across the 5 of their papers we have counts for
Showing 2026Show all
2 papers · 1 filter
cs.PL2026
Modular Composition of Inductive Types Using Lean Meta-programming
Ramy Shahin
Inductive types are ubiquitous building blocks in many programming and theorem proving languages. An inductive type is a closed set of constructors from which values of the type ca…
cs.SE2026
A Shallow Embedding of Datalog in Lean
Ramy Shahin
Datalog is a lightweight logic programming language, based on the logic of Horn clauses. Lean, on the other hand, is a proof assistant system and language based on the Calculus of…