The date for the annual meeting of the IFIP WG 1.6 is Saturday, July 18, 2026. The meeting is co-located with FSCD and IJCAR 2026, at FLoC, and will take place on the first pre-conference workshop day.
Abstract: From my work on the process interpretation of regular expressions (some jointly with Wan Fokkink, and earlier with Jos Baeten and Flavio Corradini) I want to explain several examples for where my background in rewriting, proof theory, and Lambda Calculus was instrumental in finding a solution for an open question, or at least for better understanding a problem's difficulty. The hard questions hereby concern the recognition of graphs that are bisimilar to process interpretations of regular expressions, and Milner's axiomatisation question.
The examples concern rewriting-inspired approaches rather than direct applications of rewriting theory. They will be of two sorts: (1): Formulating local simplifications of process graphs with structure constraints as small steps in order to reason about global properties (such as structure preservation/non-preservation under bisimulation collapse, decidability of expressibility by a regular expression). (2): Interpretation-readback correspondences, of varying tightness, between regular expressions (as terms) and graphs (denoting processes).
Abstract: This work proposes a method for verifying runtime errors in concurrent programs using logically constrained term rewrite systems (LCTRSs). We present a method for transforming concurrent programs with semaphores into LCTRSs and reducing runtime-error verification to the all-path reachability (APR) problem. Furthermore, we propose proof methods for proving and disproving APR problems in the style of cyclic proofs.
Abstract: Theorem proving calculi like superposition are parametrized by term and clause orderings. These orderings are used to restrict the search space, to prove the calculi complete, and to show their compatibility with redundancy deletion and simplification techniques.
Traditionally, clause orderings are defined as multiset extensions of multiset extensions of term orderings. These orderings justify almost all simplification techniques commonly found in today’s theorem provers, with one notable exception: They cannot be used to prove that superposition-like calculi are compatible with certain kinds of variable elimination. We discuss methods to partially overcome this problem and demonstrate the limits of these methods.
Abstract: In the literature one finds two views on rewriting:
We argue that it is interesting to systematically connect both views, supported by various simple examples. For instance, reducibility (the reflexive--transitive closure) in view 1 is connected to reduction (a certain free construction) in view 2. After discussing several such basic examples, we present the general pattern, with as basic intuition that view 1 corresponds to closure properties (to adjectives: reducibility, convertibility,...), and view 2 to free constructs (to nouns: reduction, conversion, ...), and conclude with discussing how this connexion is helpful, leads to new results and rewrite theory.
Abstract: We will present the new website rewriting.inria.fr which has been developed over the last years.
Abstract: We will present an overview of the 15th International School on Rewriting, held from 12 to 16 July 2026.
Abstract: A new bid will be presented for ISR 2028.
09:00--10:00: Session 1
10:30--12:15: Session 2
13:45--15:15: Session 3
15:45--17:15: Session 4
The meetings of the working group are public, with the single exception of the business meeting. The presentations are all in-person, but will be livestreamed.
Cynthia Kop and Carsten Fuhs