WPTE 2025
11th International Workshop on Rewriting Techniques for Program Transformations and Evaluation
Birmingham, UK
Sunday, July 20th, 2025
About
The aim of WPTE is to bring together 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
Submission of extended abstracts: 14th May 2025 (AoE), extended, at https://easychair.org/conferences/?conf=wpte2025
Notification of acceptance: 11th June 2025 (delayed to the 13th)
Early registration for the conference: 15th June 2025 (extended)
Final version for informal proceedings: 30th June 2025
Workshop: 20th July 2025
Submission to post-proceedings/special issue: autumn 2025 (tbd)
Invited Speakers
Programme (speakers linked)
Session 1 (09:00-10:00)
09:00-10:00: (invited talk) Transformations of Macro Tree Programs by Sebastian Maneth
Session 2 (10:30-12:30)
10:30-11:00:Refactoring Communication Protocols for Crash Safety by Leonid Nosovitskiy and Adam D. Barwell
11:00-11:30:Proving Termination of Scala Programs by Constrained Term Rewriting by Dragana Milovancevic , Carsten Fuhs and Viktor Kuncak
11:30-12:00:A Cyclic Proof System for Partial Correctness of Separation Logic with Recursive Procedure Calls by Takumi Sato and Koji Nakazawa
12:00-12:30:On Transforming Prioritized Multithreaded Programs into Logically Constrained Term Rewrite Systems by Misaki Kojima and Naoki Nishida
Session 3 (14:00-15:30)
14:00-15:00: (invited talk) Generating feedback from rewrite strategies for interactive exercises by Alex Gerdes
15:00-15:30:Probabilistic Lazy PCF with Real-Valued Choice by David Sabel and Manfred Schmidt-Schauss
Session 4 (16:00-17:30)
16:00-16:30:Towards a verified compiler for Distributed PlusCal by Ghilain Bergeron , Horatiu Cirstea and Stephan Merz
16:30-17:00:On Merging Constrained Rewrite Rules of Induction Hypotheses in Constrained Rewriting Induction by Naoki Nishida and Nozomi Taira
17:00-17:30:Bounded Rewriting Induction for LCSTRSs by Kasper Hagens and Cynthia Kop
Topics of Interest
Correctness of program transformations, optimizations and translations.
Program transformations for proving termination, confluence, and other properties.
Correctness of evaluation strategies.
Operational semantics of programs, operationally-based program equivalences such as contextual equivalences and bisimulations.
Cost-models for arguing about the optimizing power of transformations and the costs of evaluation.
Program transformations for verification and theorem proving purposes.
Translation, simulation, equivalence of programs with different formalisms, and evaluation strategies.
Program transformations for applying rewriting techniques to programs in specific programming languages.
Program transformations for program inversions and program synthesis.
Program transformation and evaluation for Haskell and rewriting.
Rewriting-based transformations for bidirectional programming and reversible computation.
For submission guidelines and publication plans, see the Call for Papers .
Program Committee
Martin Avanzini , Inria Sophia AntipolisPatrick Bahr , IT University of CopenhagenDemis Ballis , University of UdineMirai Ikebuchi , Kyoto UniversityCynthia Kop (co-chair), Radboud University NijmegenIvan Lanese , University of BolognaPierre Lermusiaux , Inria RennesSteven Libby , University of PortlandLuca Roversi , University of TurinJanis Voigtländer (co-chair), University of Duisburg-EssenJohannes Waldmann , Leipzig University of Applied SciencesSarah Winkler , Free University of Bozen-Bolzano
Steering Committee
Ștefan Ciobâcă , Alexandru Ioan Cuza University, Iași
Horatiu Cirstea , LORIA, Université de Lorraine
Santiago Escobar , Universitat Politècnica de València
Joachim Niehren , Inria Lille
Naoki Nishida , Nagoya University
David Sabel , RheinMain University of Applied Sciences, Wiesbaden
Manfred Schmidt-Schauß , Goethe-University, Frankfurt am Main
Previous WPTEs
