Confluence Competition

Overview

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 first confluence competition (CoCo 2012) will take place as part of the 1st International Workshop on Confluence (IWC 2012), which is collocated with the 23rd International Conference on Rewriting Techniques and Applications (RTA 2012) at Nagoya University, Japan. In this competition a category for first-order term rewrite systems will be run. Other categories (e.g., higher-order) will be considered if there are tools and problems.

Procedure

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. Details for the organisation of CoCo 2012 are available.

Steering Committee

• Takahito Aoto (Chair, Tohoku University, Japan)
• Nao Hirokawa (JAIST, Japan)
• Harald Zankl (University of Innsbruck, Austria)

Contact

coco-sc [AT] jaist.ac.jp

Bylaws

• The steering committee (SC) is responsible for all affairs concerning the confluence competition.
• The SC votes a chair.
• Decisions in the SC (if not by global agreement) are by simple majority vote. In case of a draw the chair decides.