WPTE 2023

10th International Workshop on Rewriting Techniques for Program Transformations and Evaluation

Rome, Italy

Part of FSCD/CADE 2023

Saturday, July 1st, 2023

Register at: https://easyconferences.eu/fscd2023/.


The aim of WPTE is to bring together the researchers working on program transformations, evaluation, and operationally based programming language semantics, using rewriting methods, in order to share the techniques and recent developments and to exchange ideas to encourage further activation of research in this area.

Important Dates

Invited Speakers

Dan Ghica, Huawei Research and Birmingham University, UK


Syntactic trinitarianism: terms, graphs, diagrams


The concept of 'syntax' is commonly understood as the structure hidden in linear sequences of tokens, which in language and logic we commonly call 'terms'. However, for the purpose of analysis and transformation, compilers use more efficient data structures to represent syntax, namely graphs. The gap between the linear (term) and graph syntax is elegantly bridged by a third formalism, namely that of string diagrams, a planar representation of terms in the categorical representation of syntax. In this tutorial talk I will show how the interplay of terms, graphs, and diagrams can help specify and implement complex analyses and transformations in compilers for higher-order programming languages, such as type inference, automatic differentiation, or closure conversion. This methodology is at the foundation of a new industrial-strength compiler being implemented currently at Huawei.

Most of the material I will discuss is based on the recent tutorial paper "Hierarchical string diagrams and applications" jointly with Fabio Zanasi.

Aart Middeldorp, University of Innsbruck, Austria


Hydra Battles, Termination, and Transformations


The Battle of Hercules and Hydra is a combinatorial game introduced by Kirby and Paris. In an influential paper they proved that the termination of the Battle cannot be established in Peano arithmetic. Several authors have modeled the Battle as a term rewrite system. In this talk we review the various encodings and some of the termination techniques used to prove the termination of the ensuing rewrite systems.

Accepted talks

Tentative Program

Session 1 (09:00-10:00)
Session 2 (10:30-12:30)
Session 3 (14:00-15:30)

Previous WPTEs

Topics of Interest

Program Committee

Steering Committee