Email Gateway (Jul 05 2026 at 18:18): Email Gateway (Jul 05 2026 at 18:18):From: Dmitriy Traytel <cl-isabelle-users@lists.cam.ac.uk>
Subject: [isabelle] New in the AFP: Certified Infinite Descent Criteria
A new entry by Jamie Wright, Liron Cohen, Reuben Rowe, and Andrei Popescu, which reminded me of Randall Munroe's rendition of Ozymandias: https://xkcd.com/1557/ . If I read the ITP program right, there will be an opportunity to hear more about this work in Lisbon.
Certified Infinite Descent Criteria
Infinite Descent is the global trace condition that underpins the soundness of cyclic reasoning and, in program analysis, the size change termination principle. Many (semi-)decision procedures for Infinite Descent are known, based on criteria ranging from automata-based constructions and relation-based characterizations, to effective (but incomplete) heuristics. We present an Isabelle/HOL mechanization of this landscape. We provide a reusable, locale-based framework of sloped graphs that defines Infinite Descent at an abstract level, independently of any concrete graph encoding. Within this framework we formalize standard complete criteria and prove their equivalence to the locale-level InfiniteDescent predicate. We also formalize tool-facing sufficient criteria, prove their soundness, and certify incompleteness where appropriate via verified counterexamples. Along the way we contribute reusable lemmas for omega-regular reasoning over streams and for Buchi-automata constructions needed by the inclusion proofs.
https://isa-afp.org/entries/Infinite_Descent_Criteria.html
Enjoy!
Last updated: Jul 22 2026 at 14:00 UTC