September 12, 2016: Confluence Competition 2016

This month the 5th Confluence Competition (CoCo 2016) took place at CLA 2016 in Obergurgl. It ran live during IWC 2016. Four confluence tools and one certifier that are developed at CL participated and won several categories (results).

Confluence is a central property of programs since it ensures uniqueness of computation results. Numerous techniques for proving confluence of rewrite systems, lambda calculi, etc. have been developed, and many of them are implemented in automated tools that (dis)prove confluence. CoCo aims to foster the development of techniques for (dis)proving confluence automatically by setting up a dedicated competition among confluence tools. Previous editions of the competition were held in Nagoya (2012), Eindhoven (2013), Vienna (2014), and Berlin (2015).

In 2016 CoCo had four competition categories

• confluence of first-order term rewrite systems (TRS)
• confluence of conditional term rewrite systems (CTRS)
• certification (CPF)
• confluence of higher-order term rewrite systems (HRS)

and tools from Innsbruck participated and won in all of them:

• CSI won the TRS category
• ConCon was the most powerful tool for CTRSs
• The certifier CeTA in combination with CSI for TRSs and with ConCon for CTRSs won the category for certified confluence proofs
• CSI^ho was the strongest tool in the higher-order category

Additionally there were three demonstration categories

• ground confluence of many-sorted term rewrite systems (GCR)
• unique normalization of term rewrite systems (UN) – new this year
• confluence of nominal rewrite systems (NRS)

with CL participation by CSI in the UN category and the newcomer FORT in both the UN and the GCR categories. All these tools are open source.