|
Published: 16th February 2018 DOI: 10.4204/EPTCS.265 ISSN: 2075-2180 |
| 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 |
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).
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.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.
February 2018,
Horatiu Cirstea and David Sabel
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.