Description

This page accompanies a paper (doi: 10.1145/3293880.3294098) presented at CPP 2019 (slides).

We present an ongoing formalization effort (in Isabelle/HOL, on top of IsaFoR) aimed at formalizing the decidability of the first-order logic of left-linear, right-ground term rewrite systems. At this point, we have executable constructions that suffice for proving (ground) confluence.

Links

• browse theory files online
• download FORTissimo theory files (updated: 2018-10-08)
  includes Haskell sources for the tools
• IsaFoR snapshot (updated: 2018-10-04)
• AFP 2018 snapshot (updated: 2018-10-04)
• experimental results: ground confluence, confluence