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. In the literature one finds two views on rewriting: 1- as relations (Dershowitz & Jouannaud, Klop, Baader & Nipkow, Ohlebusch,...), and 2- as systems (Newman,Hindley, Melliès,Khasidashvili,...). 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. 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. We will report on ISR 2026, and discuss the bid for ISR 2028.

ABSTRACT. In this presentation Luigi will show the progress of the project to develop a new goto website for rewriting.

ABSTRACT. The business meeting of the IFIP working group. This is the only part of the day that is closed to non-members.