Published: 22nd February 2019
DOI: 10.4204/EPTCS.289
ISSN: 2075-2180

EPTCS 289

Proceedings Fifth International Workshop on
Rewriting Techniques for Program Transformations and Evaluation
Oxford, England, 8th July 2018

Edited by: Joachim Niehren and David Sabel

Preface
Joachim Niehren and David Sabel
Reducing Total Correctness to Partial Correctness by a Transformation of the Language Semantics
Andrei-Sebastian Buruiană and Ştefan Ciobâcă
1
Automating the Diagram Method to Prove Correctness of Program Transformations
David Sabel
17
On Transforming Functions Accessing Global Variables into Logically Constrained Term Rewriting Systems
Yoshiaki Kanazawa and Naoki Nishida
34
Optimizing Space of Parallel Processes
Manfred Schmidt-Schauß and Nils Dallmeyer
53
On Transforming Narrowing Trees into Regular Tree Grammars Generating Ranges of Substitutions
Naoki Nishida and Yuya Maeda
68
Invited Presentation: A Framework for Graph Rewriting
Jean-Pierre Jouannaud
88

Preface

This volume contains the formal proceedings of the 5th International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2018), held on 8th of Juli 2018 in Oxford, United Kingdom, and affiliated with FLoC 2018 and FSCD 2018.

Scope of WPTE

Rewriting techniques are of great help for studying correctness of program transformations, translations and evaluation, and 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. Topics in the scope of WPTE include the correctness of program transformations, optimisations 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 reasoning 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.

Research Paper Selection

At the workshop six research papers were presented of which five were accepted for the postproceedings. Each submission was reviewed by three or four members of the Program Committee in two to three rounds, one round for workshop presentation and at most two rounds for publication to the postproceedings.

The program also included one invited talk by Jean-Pierre Jouannaud (Polytec, Palaiseau, Grand Paris, France) on a framework for graph rewriting; the abstract of this talk is included in this volume.

Acknowledgments

Many people helped to make WPTE 2018 a success. We thank the members of the program committee for their careful reviewing of all submissions and we thank the participants for their valuable contributions. We express our gratitude to all members of the local organization of FLOC 2018 under direction of Marta Kwiatkowska and the conference chair of FSCD 2018. Finally, we thank the editors of EPTCS for the publication of the post-proceedings.

Program Committee

It was a pleasure to work with the members of the program committee. We would also like the authors of the papers for all their work to make WPTE 2018 happen. And finally we hope for equally successful editions of WPTE in the following years.

With greeting to the readers of this WPTE edition.

Joachim Niehren and David Sabel

January 2019

A Framework for Graph Rewriting

Jean-Pierre Jouannaud (Polytec, Palaiseau, Grand Paris, France)

Rewriting with graphs enjoys a long history in computer science, graphs being used to represent not only data structures, but also program structures, and even computational models. Termination and confluence techniques have been elaborated for various generalizations of trees, such as rational trees, directed acyclic graphs, lambda terms and lambda graphs. But the design of tools for rewriting arbitrary graphs has made little progress beyond various categorical definitions dating from the mid seventies and the study of the particular families of graphs listed above. This paper describes the generalization of term rewriting techniques to a general class of multigraphs that we call drags, viz. finite, directed, ordered (multi-)graphs. To this end, we develop a rich algebra of drags which allows us to view graph rewriting in exactly the same way as we view term rewriting.