Fourth International Workshop on

Rewriting Techniques for
Program Transformations and Evaluation

affiliated with FSCD 2017

Oxford, UK, 8th September 2017

St Anne's College (56 Woodstock Road, OX2 6HS)

About WPTE

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 of interest in the scope of this workshop include:

The programming languages of interest include pure, deterministic, impure, nondeterministic, concurrent, parallel languages, and may employ programming paradigms such as functional, logical, typed, imperative, object-oriented, and higher-order.

This edition is affiliated with FSCD 2017.

Previous editions: WPTE 2014 (affiliated with RTA/TLCA 2014), WPTE 2015 (affiliated with RDP 2015), WPTE 2016 (affiliated with FSCD 2016)

Next edition:

The fifth edition of WPTE (WPTE 2018) will take place on 8th of July 2018 in Oxford, UK
as a FLoC 2018 workshop affiliated with FSCD 2018.
Further information can be found on the webpage of WPTE 2018.


The WPTE post-proceedings are published in Electronic Proceedings in Theoretical Computer Science ( as volume EPTCS 265.

Important Dates

Invited Speaker


09:00-09:30 Registration
09:30-11:00 Session 1 (chair: David Sabel)
09:30 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.

Efficient implementation of evaluation strategies via token-guided graph rewriting

Koko Muroya and Dan R. Ghica
11:00-11:30 Coffee break
11:30-13:00 Session 2 (chair: Horatiu Cirstea)
Reduced dependency spaces for existential parameterised Boolean equation systems

Yutaro Nagae and Masahiko Sakai

Transforming Dependency Chains of Constrained TRSs into Bounded Monotone Sequences of Integers

Tomohiro Sasano, Naoki Nishida, Masahiko Sakai and Tomoya Ueyama
Space Improvements and Equivalences in a Functional Core Language

Manfred Schmidt-Schauss and Nils Dallmeyer
13:00-14:00 Lunch
14:00-15:30 Session 3 (chair: David Sabel)
Transforming Proof Tableaux of Hoare Logic into Inference Sequences of Rewriting Induction

Shinnosuke Mizutani and Naoki Nishida
Attributed Hierarchical Port Graphs and Applications

Nneka Ene, Maribel Fernandez and Bruno Pinaud
A Method to Translate Order-Sorted Algebras to Many-Sorted Algebras

Liyi Li and Elsa Gunter
15:30-16:00 Coffee break
16:00-17:00 Session 4 (chair: Naoki Nishida)
Confluence by Strong Commutation with Disjoint Parallel Reduction

Kentaro Kikuchi
Business meeting and closing

Accepted Papers

Participation and Registration

Registration is open now and possible via the FSCD 2017 registration.

The venue of WPTE is St Anne's College (56 Woodstock Road, OX2 6HS), see FSCD 2017 Local Information and ICFP 2017, Travel to Oxford for more information on attending Oxford.

Paper Selection and Proceedings

Contributions to WPTE

For the paper submission deadline an extended abstract of at most 10 pages is required to be submitted. The extended abstract may present original work or also work in progress. However, for the formal post-proceedings (see below) full papers must be submitted to the post-proceedings deadline.
Based on the submissions the program committee will select the presentations for the workshop. All selected contributions will be included in the informal proceedings distributed to the workshop participants.
One author of each accepted extended abstract is expected to present it at the workshop. Submissions must be prepared in LaTeX using the EPTCS macro package (

Formal Proceedings

The WPTE post-proceedings are published in Electronic Proceedings in Theoretical Computer Science ( as volume EPTCS 265.

The authors of all presented contributions will have the opportunity (but no obligation) to submit a full paper for the formal post-proceedings. These full-papers must represent original work and should not be submitted to another conference at the same time. Full-papers should not exceed 15 pages. The submission deadline for these post-proceedings was after the workshop in October 2017. There was a second round of reviewing for selecting papers to be published in the formal proceedings.

Call for Papers

The call for papers is available in TXT-format.

Program Committee



Steering Committee

Last modified 2017/08/16 by D. Sabel