POPL 2025 (series) / CPP 2025 (series) / CPP 2025 /
Formalizing Simultaneous Critical Pairs for Confluence of Left-Linear Rewrite Systems
This program is tentative and subject to change.
We report on the formalization of a sufficient condition for confluence of first-order left-linear rewrite systems within the proof assistant Isabelle/HOL. This criterion, originally proposed by Okui (1998), is based on simultaneous critical pairs, which finitely represent peaks consisting of a multi-step and a normal step. It properly subsumes the formalized result on development-closed critical pairs.
This program is tentative and subject to change.
Mon 20 JanDisplayed time zone: Mountain Time (US & Canada) change
Mon 20 Jan
Displayed time zone: Mountain Time (US & Canada) change
14:00 - 15:30 | |||
14:00 30mTalk | An Isabelle formalization of co-rewrite pairs for non-reachability in conditional rewriting CPP Dohan Kim University of Innsbruck, Teppei Saito Japan Advanced Institute of Science and Technology, Japan, René Thiemann University of Innsbruck, Akihisa Yamada National Institute of Informatics | ||
14:30 30mTalk | Intrinsically Correct Sorting in Cubical Agda CPP Cass Alexandru RPTU Kaiserslautern-Landau, Vikraman Choudhury Università di Bologna & Inria OLAS, Jurriaan Rot Radboud University Nijmegen, Niels van der Weide Radboud University | ||
15:00 30mTalk | Formalizing Simultaneous Critical Pairs for Confluence of Left-Linear Rewrite Systems CPP | ||