Certification of Confluence- and Commutation-Proofs via Parallel Critical Pairs
Parallel critical pairs (PCPs) have been used to design sufficient criteria for confluence of term rewrite systems. In this work we formalize PCPs and the criteria of Gramlich, Toyama, and Shintani and Hirokawa in the proof assistant Isabelle. In order to reduce the amount of bureaucracy we deviate from the paper-definition of PCPs, i.e., we switch from a position-based definition to a context-based definition. This switch not only simplifies the formalization task, but also gives rise to a simple recursive algorithm to compute PCPs. We further generalize all mentioned criteria from confluence to commutation and integrate them in the certifier CeTA, so that it can now validate confluence- and commutation-proofs based on PCPs. Because of our results, CeTA is now able to certify proofs by the automatic confluence tool Hakusan, which makes heavy use of PCPs. These proofs include term rewrite systems for which no previous certified confluence proof was known.
Mon 15 JanDisplayed time zone: London change
14:00 - 15:30 | |||
14:00 30mTalk | A Temporal Differential Dynamic Logic Formal Embeddingremote presentation CPP | ||
14:30 30mTalk | Formal Probabilistic Methods for Combinatorial Structures using the Lovász Local Lemmadistinguished paper CPP Pre-print | ||
15:00 30mTalk | Certification of Confluence- and Commutation-Proofs via Parallel Critical Pairs CPP Nao Hirokawa Japan Advanced Institute of Science and Technology, Dohan Kim University of Innsbruck, Kiraku Shintani Japan Advanced Institute of Science and Technology, René Thiemann University of Innsbruck |