Email Gateway (Sep 12 2025 at 21:46): Email Gateway (Sep 12 2025 at 21:46):From: Dmitriy Traytel <cl-isabelle-users@lists.cam.ac.uk>
Dear all,
Anders Schlichtkrull, René Rydhof Hansen, and Flemming Nielson have formalized the semantics and a number of static analysis techniques for stratified Datalog. An unrelated language fact: in Danish “datalog" means "computer scientist” and this terminology was coined by Peter Naur. Now I wonder what a stratified computer scientist would be...
Stratified Datalog and Program Analysis
In this entry we formalize stratified Datalog, the first such formalization in Isabelle to the best of our knowledge. Next we formally establish the existence of least solutions for any stratified Datalog program, essential for reasoning about negations in clauses. Lastly we illustrate the usefulness of our Datalog formalization by further formalizing the general Bit-Vector Framework and formalize and prove correct five analyses in this framework namely liveness, reaching definitions, available expressions, very busy expressions and reachability. Many of our definitions follow Nielson and Nielson’s textbook. The formalization is described in our SAC 2024 paper.
https://www.isa-afp.org/entries/Stratified_Datalog.html
Enjoy!
Last updated: Sep 13 2025 at 04:22 UTC