[TYPES/announce] CoCo 2015: First Call for Provers

[Takahito Aoto]

======================================================================
                       First Call for Provers
                             CoCo 2015
                     4th Confluence Competition

                  2 August, 2015, Berlin, Germany
               http://coco.nue.riec.tohoku.ac.jp/2015/
======================================================================

Confluence provides a general notion of determinism and has been
conceived as one of the central properties of rewriting. Confluence
had been investigated in many formalisms of rewriting such as
first-order rewriting, lambda-calculi, higher-order rewriting,
constrained rewriting, conditional rewriting, etc.  Recently, several
new implementations of confluence tools are reported and interest for
proving/disproving confluence "automatically" has been grown. The
confluence competition aims to foster the development of techniques
for proving/disproving confluence automatically by a dedicated
competition among such tools.

The 4th Confluence Competition (CoCo 2015) will run ***live*** during
the 4th International Workshop on Confluence (IWC 2015), collocated
with CADE-25 in Berlin, Germany.

The following categories will be run:
 * TRS:  confluence of first-order term rewrite systems
 * CTRS: confluence of conditional term rewrite systems
 * CPF:  certification
 * HRS:  confluence of higher-order term rewrite systems  (new!)
Besides these categories, new competition and demonstration categories
will be considered if there are tools and problems dedicated to those
categories. Demonstration categories are for demonstrating new
attempts and/or merits of particular tools.  Submissions of new
confluence problems are also welcome. For more information including
examples of new categories to be considered, platforms, competition
rules and problems, see the webpage of CoCo 2015 indicated above.

IMPORTANT DATES:
 * request for competition categories    January 31, 2015
 * request for demonstration categories  May 31, 2015
 * tool registration                     July 19, 2015
 * tool submission                       July 26, 2015
 * problem submission                    July 28, 2015
 * competition                           August 2, 2015


REQUEST FOR NEW CATEGORIES:
Request for new categories is via the contact email address. Please send
the following information at your earliest convenience:
 * category type (competition category or demonstration category)
 * description of problems and semantics (rewrite steps, confluence, etc.)
   together with adequate references
 * a proposal of the input format (if necessary) 
Requests for new categories may be rejected for technical reasons.

SUBMISSION OF NEW PROBLEMS:
Submissions of new confluence problems are welcome. Please use the web
interface of Cops (Confluence Problems) database linked from the
webpage of CoCo 2015. The HRS extension of Cops will be available very
soon.

REGISTRATION/SUBMISSION:
Tool registration is via the contact email address. Every tool
registration should also contain a one page system description. Tool
submission will be via StarExec.

ORGANISING COMMITTEE:
 * Takahito Aoto        Tohoku University (chair)
 * Nao Hirokawa         JAIST
 * Julian Nagele        University of Innsbruck
 * Naoki Nishida        Nagoya University
 * Harald Zankl         University of Innsbruck

ADVISORY BOARD:
 * Beniamino Accattoli  INRIA, Paris
 * Yuki Chiba           JAIST

CONTACT:
  coco-sc [AT] jaist.ac.jp