[TYPES/announce] CoCo 2016: Second Call for Provers

Nao Hirokawa hirokawa at jaist.ac.jp
Fri May 20 00:52:57 EDT 2016

                     Second Call for Provers
                            CoCo 2016
                    5th Confluence Competition

                     September 8 or 9, 2016
                       Obergurgl, Austria

Confluence provides a general notion of determinism and has been
conceived as one of the central properties of rewriting. Confluence
had been investigated in several formalisms of rewriting such as
first-order rewriting, lambda-calculi, higher-order rewriting,
constrained rewriting and conditional rewriting.  In recent years the
focus in confluence research has shifted towards the development of
automatable techniques for confluence proofs.  The confluence
competition aims to foster the development of techniques for
proving/disproving confluence automatically by setting up a dedicated
competition among confluence tools.

The 5th Confluence Competition (CoCo 2016) will run ***live*** during
the 5th International Workshop on Confluence (IWC 2016), collocated
with Computational Logic in the Alps (CLA 2016) in Obergurgl, Austria.

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
Besides these categories, new categories will be considered if there
are tools and problems dedicated to those categories. We welcome
requests for 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 2016 indicated above.

* request for competition categories    February 28, 2016 (closed)
* request for demonstration categories  June 30, 2016
* tool registration                     August 21, 2016
* tool submission                       August 28, 2016
* problem submission                    August 30, 2016
* competition                           September 8 or 9, 2016

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.

Submissions of new confluence problems are welcome. Please use the web
interface of Cops (Confluence Problems) database linked from the
webpage of CoCo 2016. 

Tool registration must be made electronically through the EasyChair
system at: https://www.easychair.org/conferences/?conf=coco2016
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/HRS/Demo  (leave appropriate ones)
  URL of tool's website:                      (if there is one)

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 2016. Tool submission will be via StarExec. 

* Takahito Aoto        Niigata University (chair)
* Nao Hirokawa         JAIST
* Julian Nagele        University of Innsbruck
* Naoki Nishida        Nagoya University

* Beniamino Accattoli  INRIA, Paris
* Yuki Chiba           JAIST

 coco-sc [AT] jaist.ac.jp 

More information about the Types-announce mailing list