News
- Aug 02, 2015: Added the workshop proceedings.
- June 27, 2015: Added the workshop program.
- May 29, 2015: Invited speakers finalized.
- May 29, 2015: Closed for submissions.
- December 5, 2014: webpage created.
Background
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.
Topics
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
Proceedings
PDFProgram
- 9:00-10:00
- Lambda Calculi and Confluence from A to Z (invited talk)
- Koji Nakazawa
- 10:00-10:30
- Point-Decreasing Diagrams Revisited
- Bertram Felgenhauer
- 10:30-11:00
- Coffee Break
- 11:00-11:30
- Point-Step-Decreasing Diagrams
- Bertram Felgenhauer
- 11:30-12:00
- Infeasible Conditional Critical Pairs
- Thomas Sternagel and Aart Middeldorp
- 12:00 - 12:30
- Operational Confluence of Conditional Term Rewrite Systems
- Karl Gmeiner
- 12:30 - 14:00
- Lunch Break
- 14:00 - 15:00
- Herbrand-Confluence in the Classical Sequent Calculus (invited talk)
- Stefan Hetzl
- 15:00-15:30
- Commutation and Signature Extensions
- Nao Hirokawa
- 15:30 - 16:00
- Coffee Break
- 16:00 - 16:30
- Level-Confluence of 3-CTRSs in Isabelle/HOL
- Christian Sternagel and Thomas Sternagel
- 16:30-17:00
- Labeling Multi-Steps for Confluence of Left-Linear Term Rewrite Systems
- Bertram Felgenhauer
- 17:00-17:30
- Confluence Competition
Important Dates
| submission | May 22, 2015 (submission is now closed) |
| notification | June 12, 2015 |
| final version | July 3, 2015 |
| workshop | August 2, 2015 |
Submission
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:
Organizing Committee
- Takahito Aoto (Tohoku University)
- Ashish Tiwari (SRI International - Menlo Park, CA)
Invited Speakers
- Koji Nakazawa (Kyoto University)
- Stefan Hetzl (Vienna University of Technology)
Program Committee
- 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