12th International Workshop on Confluence
23-24 August 2023, Obergurgl
IWC 2012 IWC 2013 IWC 2014 IWC 2015 IWC 2016 IWC 2017 IWC 2018 IWC 2019 IWC 2020 IWC 2021 IWC 2022 IWC 2023
IWC 2023
Background Registration Invited Speakers Accepted Papers Proceedings Important Dates Submission Program Committee Steering Committee Previous IWCs Contact

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:

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
9: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
9: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

Proceedings

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

Previous IWCs

Contact