IWC 2012
1st International Workshop on Confluence
29 May 2012, Nagoya, Japan
Background
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 RTA 2012, the 23rd International Conference on Rewriting Techniques and Applications. During the workshop the 1st Confluence Competition (CoCo 2012) takes place.
Topics
The workshop solicits short papers/extended abstracts on the following topics:
- confluence and related properties (unique normal forms, commutation, ground confluence)
- critical pair criteria
- decidability issues
- complexity issues
- system descriptions
- certification
- applications of confluence
Invited Speakers
| Vincent van Oostrom | Utrecht University | Decreasing Proof Orders – Interpreting Conversions in Involutive Monoids |
| Yoshihito Toyama | Tohoku University | Type Introduction for Confluence Proofs |
Committees
Organising Committee
| Nao Hirokawa | Japan Advanced Institute of Science and Technology |
| Aart Middeldorp | University of Innsbruck |
| Naoki Nishida | Nagoya University |
Program Committee
| Takahito Aoto | Tohoku University | |
| Nao Hirokawa | Japan Advanced Institute of Science and Technology | (co-chair) |
| Aart Middeldorp | University of Innsbruck | (co-chair) |
| Femke van Raamsdonk | VU University Amsterdam | |
| Aaron Stump | The University of Iowa | |
| Rakesh M. Verma | University of Houston |
Important Dates
| submission | March 26, 2012 |
| notification | April 9, 2012 |
| final version | May 15, 2012 |
| workshop | May 29, 2012 |
Program
| Session 1 – invited talk (chair: Nao Hirokawa) | |
|---|---|
| 9:00 – 10:00 | Type Introduction for Confluence Proofs |
| Yoshihito Toyama | |
| Session 2 (chair: Takahito Aoto) | |
| 10:30 – 11:00 | Confluence of Non-Left-Linear TRSs via Relative Termination (Extended Abstract) |
| Dominik Klein and Nao Hirokawa | |
| 11:00 – 11:30 | A Case for Completion Modulo Equivalence |
| Kristoffer Rose | |
| 11:30 – 12:00 | A Proof Order for Decreasing Diagrams |
| Bertram Felgenhauer | |
| Session 3 – invited talk (chair: Aart Middeldorp) | |
| 13.30 – 14:30 | Decreasing Proof Orders – Interpreting Conversions in Involutive Monoids |
| Vincent van Oostrom | |
| Session 4 (chair: Yoshihito Toyama) | |
| 15:00 – 15:30 | Recording Completion for Finding and Certifying Proofs in Equational Logic |
| Thomas Sternagel, René Thiemann, Harald Zankl and Christian Sternagel | |
| 15:30 – 16:00 | Automatically Finding Non-Confluent Examples in Abstract Rewriting |
| Hans Zantema | |
| 16:00 – 16:30 | IaCOP – Interface for the Administration of Cops |
| Christian Nemeth, Harald Zankl and Nao Hirokawa | |
| Session 5 – CoCo and business meeting (chairs: Takahito Aoto, Nao Hirokawa, Aart Middeldorp) | |
| 16:45 – 18:15 | including tool presentations: |
| ACP: System Description for CoCo 2012 | |
| Takahito Aoto and Yoshihito Toyama | |
| CoCo 2012 Participant: CSI | |
| Harald Zankl, Bertram Felgenhauer and Aart Middeldorp | |
| Saigawa: A Confluence Tool | |
| Dominik Klein and Nao Hirokawa | |
| Certification of Confluence Proofs using CeTA | |
| René Thiemann | |
Proceedings