[TYPES/announce] IWC 2012 & CoCo 2012: Call for Participation and Provers

Nao Hirokawa hirokawa at jaist.ac.jp
Thu Apr 19 02:12:00 EDT 2012

This is a joint call for participation and provers for IWC 2012 and CoCo 2012.

                       Call for Participation 
                              IWC 2012 
                1st International Workshop on Confluence

         29 May 2012, Nagoya, Japan, collocated with RTA 2012

Recently there is a renewed interest in confluence research, resulting
in new techniques, tool support as well as new applications. The
workshop aims at promoting further research in confluence and related
properties. The workshop is collocated with the 23rd International 
Conference on Rewriting Techniques and Applications (RTA 2012). During 
the workshop the 1st Confluence Competition (CoCo 2012) takes place
(see below).

 * early registration   April 25, 2012 JST (GMT+9)
 * registration         May    9, 2012 JST (GMT+9)
 * workshop             May   29, 2012 JST (GMT+9)

Please register at:


 * Vincent van Oostrom  Utrecht University
 * Yoshihito Toyama     Tohoku University

 * Bertram Felgenhauer:
     A Proof Order for Decreasing Diagrams
 * Dominik Klein and Nao Hirokawa: 
     Confluence of Non-Left-Linear TRSs via Relative Termination (Extended Abstract)
 * Christian Nemeth, Harald Zankl and Nao Hirokawa:
     IaCOP - Interface for the Administration of COPS
 * Kristoffer Rose:
     A Case for Completion Modulo Equivalence
 * Thomas Sternagel, René Thiemann, Harald Zankl and Christian Sternagel:
     Recording Completion for Finding and Certifying Proofs in Equational Logic
 * Hans Zantema:
     Automatically Finding Non-Confluent Examples in Abstract Rewriting

 * Nao Hirokawa         JAIST
 * Aart Middeldorp      University of Innsbruck
 * Naoki Nishida        Nagoya University

                       Second Call for Provers
                             CoCo 2012                          
                     1st Confluence Competition

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 1st Confluence Competition (CoCo 2012) runs during 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. 

 * registration        April  1, 2012 - May 15, 2012
 * system description  April 15, 2012 - May 15, 2012
 * tool submission     May 1, 2012 - May 15, 2012
 * competition         May 29, 2012

Registration and tool submission will be via the email address:

  coco-sc [AT] jaist.ac.jp 

Tools must be able to read input files written in the old TPDB format.
The output of the tools must contain an answer in the first line
followed by some proof argument understandable for human experts. 
Valid answers are YES (the input is confluent) and NO (the input is 
not confluent). Every other answer is interpreted as the tool could 
not determine the status of the input. For more information including
competition rules, see


All registered tool authors are asked to submit a one-page system 
description paper in EasyChair style. Submission is via EasyChair at


These papers will appear in the proceedings of IWC 2012.

 * Takahito Aoto      Tohoku University       (chair)
 * Nao Hirokawa       JAIST
 * Harald Zankl       University of Innsbruck

More information about the Types-announce mailing list