July 19, 2025 - Birmingham, United Kingdom

Date

The date for the annual meeting of the IFIP WG 1.6 is Saturday, July 19, 2025. The meeting is co-located with FSCD 2025, and will take place on the first post-conference workshop day.

Aims

To support the development of rewriting in particular and the study of formal structures in computations and deductions in general.
To expand on the awareness and success of rewriting and lambda calculus in theoretical computer science.
To represent and seek cooperations between all communities working on formal structures in computations and deductions.
To foster development of applications of theoretical advances.

Invited Speakers

David Cerna
Santiago Escobar
NuITP: An Inductive Theorem Prover for Maude
Abstract: NuITP is an inductive equational theorem prover for Maude equational theories that combines advanced symbolic techniques such as narrowing, equality predicates, variant unification, variant satisfiability, order-sorted congruence closure, ordered rewriting, and strategy-based rewriting (all applied modulo axioms). Maude equational theories include expressive features such as sorts and subsorts, conditional equations and rewriting modulo axioms. This talks presents the tool, explains its most commonly used inference rules, and illustrates their use in proving the card trick benchmark.
Florian Frohn
Raúl Gutiérrez
Daniele Nantes

Preliminary Program

09:00--10:00: Session 1

Santiago Escobar

10:30--12:30: Session 2

Raúl Gutiérrez
Daniele Nantes

14:00--15:30: Session 3

Florian Frohn
Update on the International School on Rewriting

16:00--17:00: Session 4

David Cerna

17:00--17:30: Business meeting (only for members)

Participation

The meetings of the working group are public, with the single exception of the business meeting. The presentations are all in-person.

Chair and Co-Chair/Secretary

Cynthia Kop and Carsten Fuhs