POPL 2024
Sun 14 - Sat 20 January 2024 London, United Kingdom
Mon 15 Jan 2024 15:00 - 15:30 at Kelvin Lecture - Isabelle, PVS Chair(s): Dmitriy Traytel

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 Jan

Displayed time zone: London change

14:00 - 15:30
Isabelle, PVSCPP at Kelvin Lecture
Chair(s): Dmitriy Traytel University of Copenhagen
14:00
30m
Talk
A Temporal Differential Dynamic Logic Formal Embeddingremote presentation
CPP
Lauren White NASA, Laura Titolo AMA/NASA LaRC, J Tanner Slagel NASA, Cesar Munoz NASA
14:30
30m
Talk
Formal Probabilistic Methods for Combinatorial Structures using the Lovász Local Lemmadistinguished paper
CPP
Chelsea Edmonds University of Sheffield, Lawrence Paulson University of Cambridge
Pre-print
15:00
30m
Talk
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