Blogs (1) >>
POPL 2019
Sun 13 - Sat 19 January 2019 Cascais, Portugal
Tue 15 Jan 2019 11:30 - 12:00 at Sala XII - Research Papers: Rewriting, Automated Reasoning Chair(s): Andrei Popescu

Term rewriting in the presence of associative and commutative function symbols constitutes a highly expressive model of computation, which is for example well-suited to reason about parallel computations. However, it is well-known that the standard notion of termination does not apply any more: any term rewrite system containing a commutativity rule is nonterminating. Thus, instead of adding AC-rules to a rewrite system and trying to prove termination, we switch to the notion of AC-termination. AC-termination can for example be shown using well-founded AC-compatible reduction orders. One specific example of such an order is ACKBO. We present our Isabelle/HOL formalization of the ACKBO order. On an abstract level this gives us a mechanized proof of the fact that ACKBO is indeed an AC-compatible reduction order. Moreover, we integrated corresponding check functions into the verified certifier CeTA. This has the more practical consequence of enabling the machine certification of AC-termination proofs generated by automated termination tools.

Tue 15 Jan

Displayed time zone: Belfast change

11:00 - 12:30
Research Papers: Rewriting, Automated ReasoningCPP at Sala XII
Chair(s): Andrei Popescu Middlesex University, London
11:00
30m
Research paper
Autosubst 2: Reasoning with Multi-Sorted de Bruijn Terms and Vector Substitutions
CPP
Kathrin Stark Saarland University, Germany, Steven Schäfer Saarland University, Jonas Kaiser
DOI
11:30
30m
Research paper
Certified ACKBO
CPP
Alexander Lochmann , Christian Sternagel University of Innsbruck, Austria
DOI
12:00
30m
Research paper
A Verified Ground Confluence Tool for Linear Variable-Separated Rewrite Systems in Isabelle/HOL
CPP
DOI