[isabelle] IWC 2015 (2nd CFP) and CoCo 2015 (2nd CFP)

Maybe of interest for some on this list (especially the "certification" part):

                        Second Call for Papers
                              IWC 2015
               4th International Workshop on Confluence

                    2 August 2015, Berlin, Germany
                      collocated with CADE-25


Confluence provides a general notion of determinism and has been
conceived as one of the central properties of rewriting
systems. Confluence relates to many topics of rewriting (completion,
modularity, termination, commutation, etc.) and had been investigated
in many formalisms of rewriting such as first-order rewriting,
lambda-calculi, higher-order rewriting, constraint rewriting,
conditional rewriting, etc. Recently there is a renewed interest in
confluence research, resulting in new techniques, tool support,
confluence competition, and certification as well as in new
applications. The scope of the workshop is all these aspects of
confluence and related topics.  The goal of the workshop is to provide
a forum for researchers interested in the topic of confluence to
exchange and share new developments in the field. The workshop will
enable discussion on theoretical results, new problems, applications,
implementations and benchmarks, and share the current state-of-the-art
on the development of confluence tools.  The workshop is collocated
with CADE-25. Previous editions of the workshop were held in Nagoya
(2012), Eindhoven (2013) and Vienna (2014).  During the workshop the
4th Confluence Competition (CoCo 2015) takes place.

 * submission          May  15, 2015
 * notification        June 12, 2015
 * final version       July 3, 2015
 * workshop            August 2, 2015

Specific topics of interest include:
 * confluence and related properties (unique normal forms, commutation,
   ground confluence)
 * completion
 * critical pair criteria
 * decidability issues
 * complexity issues
 * system descriptions
 * certification
 * applications of confluence

 * Koji Nakazawa (Kyoto University)

 *  Takahito Aoto (Tohoku University), co-chair
 *  Mauricio Ayala Rincon (Universidade de Brasilia)
 *  Karl Gmeiner (UAS Technikum Wien)
 *  Samuel Mimram (ÂÂÂcole Polytechnique)
 *  Haruhiko Sato (Hokkaido University)
 *  Christian Sternagel (Universtity of Innsbruck)
 *  Ashish Tiwari (SRI International - Menlo Park, CA), co-chair

We solicit short papers or extended abstracts of at most five pages.
There will be no formal reviewing. In particular, we welcome short
versions of recently published articles and papers submitted elsewhere.
The program committee checks relevance and may provide additional
feedback. The accepted papers will be made available electronically
before the workshop.

The page limit for papers is 5 pages in EasyChair style. Short
papers or extended abstracts must be submitted electronically
through the EasyChair system at:

                       Second Call for Provers
                             CoCo 2015
                     4th Confluence Competition

                  2 August, 2015, Berlin, Germany

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 demonstration categories
will be considered if there are tools and problems dedicated to those
categories. These 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.

 * 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 is via the contact email address. Please send
the following information at your earliest convenience:
 * category type (demonstration category only)
 * 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 2015. The HRS extension of Cops is also available.

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.

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

 * Beniamino Accattoli  INRIA, Paris
 * Yuki Chiba           JAIST

  coco-sc [AT] jaist.ac.jp

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.