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!
Email Gateway (Sep 13 2025 at 07:56):From: Alex Shkotin <alex.shkotin@gmail.com>
Dear Dmitriy,
Definition may be like this "Computer scientist is stratified iff she works
simultaneously in two or more projects in different sciences or
technologies."
NB: If sciences or technologies are the same he is just busy.
Enjoyed!
Alex
сб, 13 сент. 2025 г. в 00:46, 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: Oct 08 2025 at 20:22 UTC