Published: 16th February 2018
DOI: 10.4204/EPTCS.265
ISSN: 2075-2180

EPTCS 265

Proceedings Fourth International Workshop on
Rewriting Techniques for Program Transformations and Evaluation
Oxford, UK, 8th September 2017

Edited by: Horatiu Cirstea and David Sabel

Preface
Invited Talk: The Sufficiently Smart Compiler can Prove Theorems!
Joachim Breitner
1
Attributed Hierarchical Port Graphs and Applications
Nneka Chinelo Ene, Maribel Fernández and Bruno Pinaud
2
A Method to Translate Order-Sorted Algebras to Many-Sorted Algebras
Liyi Li and Elsa Gunter
20
Transforming Proof Tableaux of Hoare Logic into Inference Sequences of Rewriting Induction
Shinnosuke Mizutani and Naoki Nishida
35
Efficient Implementation of Evaluation Strategies via Token-Guided Graph Rewriting
Koko Muroya and Dan R. Ghica
52
Reduced Dependency Spaces for Existential Parameterised Boolean Equation Systems
Yutaro Nagae and Masahiko Sakai
67
Transforming Dependency Chains of Constrained TRSs into Bounded Monotone Sequences of Integers
Tomohiro Sasano, Naoki Nishida, Masahiko Sakai and Tomoya Ueyama
82
Space Improvements and Equivalences in a Functional Core Language
Manfred Schmidt-Schauß and Nils Dallmeyer
98

Preface

This volume contains the formal proceedings of the 4th International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2017), held on 8th September 2017 in Oxford, United Kingdom, and affiliated with the Second International Conference on Formal Structures for Computation and Deduction (FSCD 2017).

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, 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 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.

For this edition of the workshop seven regular research papers were accepted out of the submissions. Each submission was reviewed by at least three members of the Program Committee. The program also included one invited talk by Joachim Breitner (University of Pennsylvania, USA); the abstract of this talk is included in this volume together with the regular papers.

Acknowledgments

Many people helped to make WPTE 2017 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 FSCD 2017 and in particular to Jamie Vicary, workshop chair of FSCD 2017, and Sam Staton, conference chair of FSCD 2017, for their constant support. Finally, we thank the editors of EPTCS for the publication of the post-proceedings.

Program Committee

Beniamino Accattoli, INRIA, France
Martin Avanzini, University of Innsbruck, Austria
Yuki Chiba, JAIST, Japan
Horatiu Cirstea, LORIA, Université de Lorraine, France
Fer-Jan de Vries, University of Leicester, UK
Santiago Escobar, Politècnica de València, Spain
Maribel Fernández, King's College London, UK
Delia Kesner, Université Paris-Diderot, France
Sergueï Lenglet, Université de Lorraine, France
Elena Machkasova, University of Minnesota, Morris, USA
William Mansky, Princeton University, USA
Joachim Niehren, INRIA Lille, France
Naoki Nishida, Nagoya University, Japan
David Sabel, Goethe-University Frankfurt am Main, Germany
Masahiko Sakai, Nagoya University, Japan
Manfred Schmidt-Schauß, Goethe-University Frankfurt am Main, Germany
Janis Voigtländer, Universität Duisburg-Essen, Germany
Johannes Waldmann, HTWK Leipzig, Germany

External Reviewers

Martin Lange
Michael Schaper
Vincent Van Oostrom

February 2018,
Horatiu Cirstea and David Sabel


Invited Talk: The Sufficiently Smart Compiler can Prove Theorems!

Joachim Breitner

After decades of work on functional programming and on interactive theorem proving, a Haskell programmer who wants to include simple equational proofs in his code, e.g. that some Monad laws hold, is still most likely to simply do the proof by hand, as all the advanced powerful proving tools are inconvenient.

But one powerful tool capable of doing (some of) these proofs is hidden in plain sight: GHC, the Haskell compiler! Its optimization machinery, in particular the simplifier, can prove many simple equations all by himself, simply by compiling both sides and noting that the result is the same. Furthermore, and crucially to make this approach applicable to more complicated equations, the compiler can be instructed to do almost arbitrary symbolic term rewritings by using Rewrite Rules.

In this hands-on talk I will show how, with a very small amount of plumbing, I can conveniently embed the proof obligations for the monad laws for a non-trivial functor in the code, and have GHC prove them to me. I am looking forward to a discussion of the merits, limits and capabilities of this approach.