IWC 2023 - 12th International Workshop on Confluence
23rd and 24th August 2023, Obergurgl, Austria
Co-located with WST 2023
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 has been investigated in many formalisms of rewriting, such as first-order rewriting, lambda-calculi, higher-order rewriting, constraint rewriting, conditional rewriting, and so on. 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.
Topics are thus:
confluence, unique normal forms, commutation, ground confluence, completion, critical pair criteria, decidability issues, complexity issues, certification, applications of confluence
The 12th Confluence Competition CoCo 2023 will run live during IWC 2023.
Registration
Registration is possible via the following website: http://cl-informatik.uibk.ac.at/events/osr-2023/.
Note that early registration ends on July 15.
Invited Speakers
Naoki Nishida, Nagoya University, Japan
Unravelings and Narrowing Trees Towards Confluence of Deterministic CTRSs
In this talk, we present two main techniques developed in CO3, a COnverter for proving COnfluence of COnditional term rewrite systems, for proving confluence and infeasibility problems of deterministic conditional term rewrite systems (DCTRSs, for short). One is unraveling transformations: An unraveling is a reduction-preserving transformation of a join or oriented CTRS into a term rewrite system (TRS, for short); for a syntactically deterministic CTRS, if the unraveled TRS of the CTRS is weakly left-linear and confluent, then the CTRS is confluent. The other is narrowing trees: A narrowing tree of finitely many oriented conditions represent the set of substitutions satisfying all the conditions w.r.t. constructor-based rewriting; for a conditional critical pair of a DCTRS, if the unraveled TRS of the DCTRS is right-linear and a narrowing tree of the conditional part represents the empty set, then the conditional critical pair is infeasible.
René Thiemann, University of Innsbruck
History and Future of the CeTA-Certifier for CoCo - Including a New Decision Procedure for Pattern Completeness
This talk is split into two parts. In the first part we will provide some history of CeTA, the certifier that is used to validate the generated proofs of the annual confluence competition CoCo. In the second part we present some future plans of CeTA. Here, we present some initial steps that have been done to support ground confluence proofs. For instance, we developed a new and simple algorithm to decide pattern completeness for first-order TRSs. This property implies quasi-reducibility, a prerequisite if one wants to prove ground confluence by rewriting induction.
Program
Wednesday, August 23
| Time | Item |
|---|---|
| 09:00 -10:00 | Invited talk: Naoki Nishida Unravelings and Narrowing Trees Towards Confluence of Deterministic CTRSs |
| 10:00 - 10:30 | Fabian Mitterwallner, Jonas Schöpf and Aart Middeldorp Reducing Confluence of LCTRSs to Confluence of TRSs (paper, slides) |
| 10:30 - 11:00 | coffee break |
| 11:00 - 11:30 | Claudio Sacerdoti Coen and Riccardo Treglia Confluence of a Computational Lambda Calculus for Higher-Order Relational Queries (paper, slides) |
| 11:30 - 12:00 | Vincent van Oostrom Residuation = Skolemised Confluence (paper, slides) |
| 12:30 - 14:00 | lunch |
| 14:00 - 14:30 | Ievgen Ivanov On Confluence Criteria for Non-terminating Abstract Rewriting Systems (paper, slides) |
| 14:30 - 15:00 | Takahito Aoto, Nao Hirokawa, Dohan Kim, Misaki Kojima, Aart Middeldorp, Fabian Mitterwallner, Naoki Nishida, Teppei Saito, Jonas Schöpf, Kiraku Shintani, René Thiemann and Akihisa Yamada A New Format for Rewrite Systems (paper) |
| 15:00 - 15:30 | Christina Kohl and Aart Middeldorp Formalizing Confluence and Commutation Criteria Using Proof Terms (paper) |
| 15:30 - 16:00 | coffee break |
| 16:00 - ? | Aart Middeldorp Confluence Competition 2023 (slides) |
Thursday, August 24
| Time | Item |
|---|---|
| 09:00 -10:00 | Invited talk: René Thiemann History and Future of the CeTA-Certifier for CoCo - Including a New Decision Procedure for Pattern Completeness (paper, slides) |
| 10:00 - 10:30 | Aart Middeldorp, Masahiko Sakai and Sarah Winkler Ground Canonical Rewrite Systems Revisited (paper, slides) |
| 10:30 - 11:00 | coffee break |
| 11:00 - 11:30 | Vincent van Oostrom The Z-property for left-linear term rewriting via convective context-sensitive completeness (paper, slides) |
| 11:30 - 12:00 | Johannes Niederhauser, Nao Hirokawa and Aart Middeldorp Church–Rosser Modulo for Left-Linear TRSs Revisited (paper, slides) |
| 12:00 - 12:30 | business meeting and CoCo award ceremony (slides) |
| 12:30 - 14:00 | lunch |
Proceesings
The proceedings are available online and include reports on the Confluence Competition 2023.
Important Dates
submission (abstract): Sunday, 7th May, 2023 Sunday, 21st May, 2023
submission (paper): Sunday, 14th May, 2023 Sunday, 28th May, 2023
notification: Sunday, 11th June, 2023 Thursday, 15th June, 2023
workshop: Wednesday, 23rd and Thursday, 24th August 2023
(deadlines are AoE)
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. Submission is electronically through
https://www.easychair.org/conferences/?conf=iwc23
Program Committee
- Patrick Bahr, IT University of Copenhagen
- Cyrille Chenavier, Université de Limoges
- Benjamin Dupont, University of Grenoble Alpes
- Jörg Endrullis, Vrije Universiteit Amsterdam
- Claudia Faggian, CNRS, Université de Paris
- Carsten Fuhs, Birkbeck University of London
- Raúl Gutiérrez, Universidad Politécnica de Madrid
- Dohan Kim, University of Innsbruck
- Sarah Winkler, Free University of Bozen-Bolzano
IWC Steering Committee
Previous IWCs
1st IWC, Nagoya, 2012
2nd IWC, Eindhoven, 2013
3rd IWC, Vienna, 2014
4th IWC, Berlin, 2015
5th IWC, Obergurgl, 2016
6th IWC, Oxford, 2017
7th IWC, Oxford, 2018
8th IWC, Dortmund, 2019
9th IWC, Paris, 2020
10th IWC, Buenos Aires/online, 2021
11th IWC, Haifa, 2022
Contact
Cyrille Chenavier: cyrille.chenavier(at)unilim.fr
Sarah Winkler: winkler(at)inf.unibz.it
IWC 2023 – 12th International Workshop on Confluence - Obergurgl
Proceedings
Program Chairs
- Cyrille Chenavier - University of Limoges
- Sarah Winkler - University of Bolzano
Invited Speakers
- Naoki Nishida - Nagoya University
- René Thiemann - University of Innsbruck