14th International Workshop on Confluence
2-3 September, 2025, Leipzig
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 2024 IWC 2025
IWC 2025
Background Registration Invited Speakers Accepted Papers Program new! Local Info. & Schedule new! Important Dates Submission Program Committee Steering Committee Previous IWCs Contact

IWC 2025

14th International Workshop on Confluence

2nd - 3rd September, 2025, Leipzig, Germany

Co-located with WST 2025

News

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 14th Confluence Competition CoCo 2025 will run live during IWC 2025.

Registration

Registration is possible via the following website: https://www.imn.htwk-leipzig.de/WST2025/registration/.

Note that early registration ends on July 23, 2025.

Invited Speakers

Salvador Lucas, Universitat Politècnica de València
Confluence of Conditional Rewriting Modulo

Sets of equations E play an important computational role in rewriting-based systems R by defining an equivalence relation =E inducing a partition of terms into E-equivalence classes on which rewriting computations, denoted →R/E and called rewriting modulo E, are issued. This paper investigates confluence of →R/E, usually called E-confluence, for conditional rewriting-based systems, where rewriting steps are determined by conditional rules. We rely on Jouannaud and Kirchner's framework to investigate confluence of an abstract relation R modulo an abstract equivalence relation E on a set A. We show how to particularize the framework to be used with conditional systems. Then, we show how to define appropriate finite sets of conditional pairs to prove and disprove E-confluence. Our results apply to well-known classes of rewriting-based systems. In particular, to Equational (Conditional) Term Rewriting Systems.

Vincent van Oostrom, University of Sussex
Conway’s Game of Life and other orthogonal rewrite systems
abstract new!

We show how Conway's Game of Life (GoL) can be modelled by means of orthogonal graph rewriting. More precisely, we model GoL by means of a graph rewrite system where each cell of the grid is represented by a node having 8 ports, each linked to one of its 8 neighbouring nodes. A rewrite rule then lets a node cyclically rotate its principal port to the next (either widdershins or deosil) port while updating its alive-neighbour-count. After a full rotation, its state is updated accordingly. We show this yields a graph rewrite system (GRS) where computing the next GoL-iteration may be achieved in 8 ticks by means of what we call ©locksteps better known in rewriting as full multisteps contracting all redex-patterns in the graph in parallel. The GRS being orthogonal liberates one from having to perform ©locksteps only, to always contract all redex-patterns: orthogonality makes that redex-patterns may be contracted asynchronously, even one at the time, need not be contracted in lockstep. There are no clogsteps (so to speak), making the modelling ideally suited for implementation on GPUs.

In the second part of the presentation we show in what sense the graph rewrite system used to model GoL in the first part is orthogonal. We show it constitutes a so-called Interaction Net (IN) and that a (single) step from graph G to graph H with respect to rule rule ρ : L → R can be decomposed into three phases:

  1. the matching phase, an SC-expansion GSC↞ C[L] exhibiting the to-be-replaced substructure L within G;
  2. the replacement C[L] → C[R] of the exihibited substructure L, left-hand side of rule ρ, by its right-hand side R;
  3. the substitution phase, an SC-reduction C[R] ↠SC H plugging-in the substructure R yielding H.
Here SC stands for Substitution Calculus, the calculus used for abstracting subgraphs into variables and substituting for them again (matching and substitution). In the case of INs the SC is particularly simple, and consists essentially in managing indirection nodes. We exemplify this decomposition extends to term rewrite systems (TRSs; having the simply typed λαβη-calculus as SC) and to term graph rewrite systems (TGRSs; having an SC, the ж-calculus, based on sharing), putting INs on a par with orthogonal TRSs and orthogonal TGRSs, thereby unlocking the theory of orthogonality to GoL and other cellular automata. For instance, that INs are confluent, even has least upperbounds, is an immediate consequence of orthogonality (confluence-by-parallelism).

References: there being an abundance of literature on Game of Life and on Interaction Nets, we only give references to the lesser-known approach to structured rewriting by means of Substitution Calculi: van Oostrom, PhD thesis, VUA, 1994, van Raamsdonk, PhD thesis, VUA, 1996, Hirokawa, Nagele, van Oostrom, Oyamaguchi, CADE, 2019, van Oostrom, HOR, 2025.

Aart Middeldorp, University of Innsbruck
Termination and Confluence: Remembering Hans Zantema (Joint IWC and WST Invited Talk)

In this presentation I give an incomplete overview of the many contributions of Hans Zantema to termination and confluence. Several of these were presented at earlier workshops on termination and confluence, and I include a biased overview of the development of these workshops and associated competitions.

Accepted Papers

Program new!

See also IWC and WST local information and schedule.

  Tuesday, September 2
Session 1 (chair: Naoki Nishida)
9:00-10:00   Vincent van Oostrom (Invited talk)
  Conway’s Game of Life and other orthogonal rewrite systems
10:00-10:30 coffee break
Session 2 (chair: Carsten Fuhs)
10:30-11:00 Jonas Schöpf and Aart Middeldorp
  Improving Confluence Analysis for LCTRSs
11:00-11:30 Johannes Niederhauser and Aart Middeldorp
  Towards Confluence of Deterministic Higher-Order Pattern Rewrite Systems by Critical Pairs
11:30-12:00 Makoto Hamana and Koko Muroya
  Term Evaluation Systems with Refinements for Contextual Improvement by Critical Pair Analysis
12:00-12:30 Rémy Cerda and Lionel Vaux Auclair
  Confluence of 001- and 101-infinitary λ-calculi by linear approximation
12:30-14:00 lunch
Session 3 (chair: Raúl Gutiérrez)
14:00-15:00 Salvador Lucas (Invited talk)
  Confluence of Conditional Rewriting Modulo
15:00-15:30 René Thiemann and Akihisa Yamada
  Deciding pattern completeness in non-deterministic polynomial time
15:30-16:00 coffee break
Session 4
16:00-17:00 Confluence Competition 2025
17:00-17:30 Business meeting
  Wednesday, September 3
Session 5 (chair: René Thiemann)
9:00-9:30 Raúl Gutiérrez and Salvador Lucas
  Proving and disproving feasibility with infChecker
9:30-10:00 Vincent van Oostrom
  Redeeming Newman; orthogonality in rewriting; Past, present and future in a 1-algebraic setting
10:00-10:30 coffee break
Session 6 (= WST Session 1)
10:30-11:30 Aart Middeldorp (IWC/WST joint Invited talk)
  Termination and Confluence: Remembering Hans Zantema
11:30-11:45 short break
WST Session 2 11:45-12:45
12:45-14:00 lunch
WST Session 3 14:00-15:30
15:30-16:00 coffee break
Departure for Excursion and Dinner 16:00

Important Dates

submission (abstract): 1st June, 2025 8th June, 2025 (extended!)
submission (paper): 1st June, 2025 8th June, 2025 11th June, 2025 (extended again!)
notification: 30th June, 2025 7th July, 2025
early registration: 23rd July, 2025
final version: 31st July, 2025
workshop: 2nd-3rd September 2025

(deadlines are AoE)

Submission

We solicit short papers or extended abstracts of at most five pages excluding references. 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 (excluding references, but 6 pages in total) in EasyChair style (6 pages excluding references, but 7 pages in total in the final version). Submission is electronically through

https://easychair.org/conferences/?conf=iwc2025

Program Committee

Previous IWCs

Contact