Confluence Competition

Confluence Competition


Confluence is considered to be one of the central properties of a program since it ensures uniqueness of computations. Numerous results have been obtained on proving the confluence of rewrite systems, lambda calculi, etc. Recently, several new implementations of confluence proving/disproving tools are reported and interest for proving/disproving confluence "automatically" has been grown. CoCo aims to foster the development of techniques for proving/disproving confluence automatically by setting up a dedicated and fair confluence competition among confluence proving/disproving tools.

The 4th confluence competition (CoCo 2015) will be collocated with CADE-25 in Berlin, Germany. Previous editions of the competition were held in Nagoya (2012), Eindhoven (2013) and Vienna (2014).


The competition will be run completely automatically on a dedicated host. For the competition a set of confluence problems is submitted to each participating tool. Each tool is supposed to answer whether the given term rewriting system is confluent or not (in a fixed time). Each tool must give evidence for its answer in a human understandable format. The tool which correctly answers the maximum number of problems wins. In the first and second competitions, categoies for first-order term rewrite systems and for certification have been run. Other categories (e.g., higher-order) will be considered if there are tools and problems.

Steering Committee

Advisory Board


coco-sc [AT]


Former Members