Confluence Competition

CoCo 2018

News

July 12, 2018: Competition finished.
July 12, 2018: watch live here.
Jun 18, 2018: Entrants are added.
May 31, 2018: Final CFP is announced.
May 9, 2018: 2nd CFP is announced.
April 12, 2018: It is fixed that the competition will run in FSCD 2018.
Dec 26, 2017: 1st CFP is announced.
Dec 26, 2017: This page is created.

Results

Slides, details, details on StarExec, and results of CoCo 2018. Congratulations to the winners: CSI (TRS, NFP and UNR categories), CSI+CeTA (CPF-TRS and CPF categories), ConCon (CTRS category), ConCon+CeTA (CPF-CTRS category), ACP (UNC and UN categories) and AGCP (GCR category).

Background

This site lists relevant information for the 7th Confluence Competition (CoCo 2018). The competition will run live during the 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018) in Oxford, United Kingdom. CoCo 2018 will be part of the FLoC 2018 Olympic Games. We invite everyone developing confluence (and related) tools to join CoCo 2018, to share problems and challenges.

Categories

The following categories will be run:

For the details (input, problem, etc.) of each category, check the category page. The CPF and UN categories are combined categories, and all of their component categories will be run. Furthermore, a demonstration category for confluence of polymorphic second-order computation systems will be run. (canceled)

Timeline

request for competition categoriesJanuary 28, 2018
request for demonstration categoriesApril 29, 2018
tool registrationJune 14, 2018
tool submissionJune 24, 2018
problem submissionJune 28, 2018
competitionJuly 12, 2018

Database

Submissions of new problems are welcome. Submissions are via Cops. Problems submitted after the problem submission deadline will not be considered for the competition. For problem selection of each category, check the detail of each category from category page.

Execution Platform

CoCo 2018 will run on StarExec, a high-end cross-community competition platform. Details of the specification are available here. For each problem a tool will have 60 seconds access to a single node.

Request for Categories

We solicit new categories for the competition (competition categories) as well as demonstration categories. See here to send your request.

Tools

Tools must be able to run on the designated execution platform. It is encouraged that tools are open source and that binaries of the competition versions of the tools can be archived on the competition website; they shall be used in our web interface in future.

Registration/Submission

Tool registration will be via EasyChair. Every tool registration should also contain a one page system description. Tool registration must be made electronically through the EasyChair system at: https://www.easychair.org/conferences/?conf=coco2018. Specify tool name as the title and tool authors as the authors. Please use the following form for the abstract:

Categories to enter: TRS/CTRS/CPF-TRS/CPF-CTRS/HRS/GCR/UNC/UNR/NFP/Demo  (leave appropriate ones)
URL of tool's website:                      (if there is one)

Entrants for CPF-TRS or CPF-CTRS category automatically enter the CPF category, and those for UNC, UNR or NFP category automatically enter the UN category. Please submit one page system description in EasyChair LaTeX class style highlighting the distinctive features of the prover (in a single latex file). System descriptions will be included in the proceedings of IWC 2018. Tool submission will be via StarExec.

Entrants

toolcategoriesauthors
ACP TRS/CTRS/CPF-TRS/UNC Takahito Aoto (Niigata University)
Yoshihito Toyama (Tohoku University)
paper slides tools:
ACP, ACP(UNC), ACP and CeTA
AGCP GCR Takahito Aoto (Tohoku University)
Yoshihito Toyam (Tohoku University)
paper slides tool
CeTA CPF-TRS/CPF-CTRS Bertram Felgenhauer (University of Innsbruck)
Franziska Rapp (Allgemeines Rechenzentrum Innsbruck)
Christian Sternagel (University of Innsbruck)
Sarah Winkler (University of Innsbruck)
paper slides tools:
ACP and CeTA,
ConCon and CeTA,
CSI and CeTA
CO3 CTRS Naoki Nishida (Nagoya University)
Yuta Tsuruta (Nagoya University)
Yoshiaki Kanazawa (Nagoya University)
paper slides tool
CoLL-Saigawa TRS Kiraku Shintani (JAIST)
Nao Hirokawa (JAIST)
paper slides tool
ConCon CTRS/CPF-CTRS Thomas Sternagel (DVT Innsbruck)
Christian Sternagel (University of Innsbruck)
Aart Middeldorp (University of Innsbruck)
paper slides tools:
ConCon, ConCon and CeTA
CSI TRS/CPF-TRS/UNC/UNR/NFP Bertram Felgenhauer (University of Innsbruck)
Aart Middeldorp (University of Innsbruck)
Fabian Mitterwallner (University of Innsbruck)
Julian Nagele (Queen Mary University of London)
paper slides tools:
CSI, CSI and CeTA
CSI^ho HRS Julian Nagele (Queen Mary University of London)
paper slides tool
FORT GCR/UNC/UNR/NFP Franziska Rapp (Allgemeines Rechenzentrum Innsbruck)
Aart Middeldorp (University of Innsbruck)
paper slides tool
SOL HRS Makoto Hamana (Gunma University)
Kentaro Kikuchi (Tohoku University)
paper slides tool

Organising Committee