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 I want to explain several examples for where my background in rewriting, proof theory, and Lambda Calculus was instrumental in finding a solution, or getting closer to one. The hard questions hereby concern, first, the recognition of graphs that are isomorphic to, and respectively bisimilar to, process interpretations of regular expressions.
The examples concern approaches and ideas inspired from rewriting and proof theory more than direct applications of results. They will mainly 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 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).
(*) Some of it with coauthors: importantly with Wan Fokkink, and earlier with Flavio Corradini and Jos Baeten.
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: Reversible computing, by allowing computation to backtrack, comes with the promise of lower energy consumption, built-in traceability, and in general provides a better understanding of e.g., causality.
Universal techniques enabling backward computation in any model exist, but developing efficient and tailored reversible models poses a set of nuanced challenges that are directly linked to the intricacies of the computational model at hand.
This long-standing problem has been addressed for a variety of models, ranging from high-level programming languages to low-level abstract machines, by either restricting expressivity to injective functions, or by logging the required information to undo computation steps.
In this talk, I will discuss ongoing work on how to leverage this latter technique to develop a reversible operational semantics for the λ-calculus that is simple, imposes no additional restriction to the initial semantics, and is optimal as it collects just enough information.
We discuss how rewriting techniques and ideas when applied to such intricate computational model allow for a cleaner presentation of such semantics. For instance, applications include proving that our backward semantics is sound and universal for all (forward) reduction strategy, and provide an efficient implementation of this operational semantics based on a graph rewriting mechanism.
Abstract: TBA
09:00--10:00: Session 1
10:30--12:30: Session 2
14:00--15:30: Session 3
16:00--17:30: 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