Program Transformations and Evaluation

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:

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

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)

- Submission deadline (extended abstracts):
~~July 14th, 2017~~**July 21st, 2017 (Extended!)**

via https://easychair.org/conferences/?conf=wpte2017. - Notification of acceptance: August 4th, 2017
- Deadline for participant proceedings: August 11th, 2017
- Workshop: September, 8th, 2017, Oxford UK
- Submission deadline for post proceedings (full-papers): October, 2017 (exact date to be announced)

- Joachim Breitner (University of Pennsylvania, USA)

- 09:00-09:30 Registration
- 09:30-11:00 Session 1

09:30 Invited Talk The sufficiently smart compiler can prove theorems! Joachim Breitner

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

10:30 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

11:30 Reduced dependency spaces for existential parameterised Boolean equation systems Yutaro Nagae and Masahiko Sakai

12:00 Transforming Dependency Chains of Constrained TRSs into Bounded Monotone Sequences of Integers Tomohiro Sasano, Naoki Nishida, Masahiko Sakai and Tomoya Ueyama

12:30 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

14:00 Transforming Proof Tableaux of Hoare Logic into Inference Sequences of Rewriting Induction Shinnosuke Mizutani and Naoki Nishida

14:30 Attributed Hierarchical Port Graphs and Applications Nneka Ene, Maribel Fernandez and Bruno Pinaud

15:00 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

16:00 Confluence by Strong Commutation with Disjoint Parallel Reduction Kentaro Kikuchi

16:30 Business meeting and closing

- Shinnosuke Mizutani and Naoki Nishida:

*Transforming Proof Tableaux of Hoare Logic into Inference Sequences of Rewriting Induction* - Kentaro Kikuchi:

*Confluence by Strong Commutation with Disjoint Parallel Reduction* - Yutaro Nagae and Masahiko Sakai:

*Reduced dependency spaces for existential parameterised Boolean equation systems* - Liyi Li and Elsa Gunter:

*A Method to Translate Order-Sorted Algebras to Many-Sorted Algebras* - Tomohiro Sasano, Naoki Nishida, Masahiko Sakai and Tomoya Ueyama:

*Transforming Dependency Chains of Constrained TRSs into Bounded Monotone Sequences of Integers* - Manfred Schmidt-Schauss and Nils Dallmeyer:

*Space Improvements and Equivalences in a Functional Core Language* - Koko Muroya and Dan R. Ghica:

*Efficient implementation of evaluation strategies via token-guided graph rewriting* - Nneka Ene, Maribel Fernandez and Bruno Pinaud:

*Attributed Hierarchical Port Graphs and Applications*

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

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 (http://style.eptcs.org/).

The WPTE post-proceedings will be published in Electronic Proceedings in Theoretical Computer Science (http://eptcs.org/).
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 will be after the workshop in October 2017.
There will be a second round of reviewing for selecting papers to be published in the formal proceedings.

The *call for papers* is available in
TXT-format.

- Beniamino Accattoli (INRIA)
- Martin Avanzini (University of Innsbruck)
- Yuki Chiba (JAIST)
- Horatiu Cirstea (LORIA, Université de Lorraine) -- chair
- Santiago Escobar (Universitat Politècnica de València)
- Maribel Fernandez (KCL)
- Delia Kesner (Université Paris-Diderot)
- Sergueï Lenglet (Université de Lorraine)
- Elena Machkasova (University of Minnesota, Morris)
- William Mansky (Princeton University)
- Joachim Niehren (INRIA Lille)
- Naoki Nishida (Nagoya University)
- David Sabel (Goethe-University Frankfurt am Main) -- chair
- Masahiko Sakai (Graduate School of Infomation Science, Nagoya University)
- Manfred Schmidt-Schauss (Goethe-University Frankfurt am Main)
- Janis Voigtländer (University of Nijmegen)
- Johannes Waldmann (HTWK Leipzig)
- Fer-Jan de Vries (University of Leicester)

- Horatiu Cirstea (LORIA, Université de Lorraine, France)
- David Sabel (Goethe-University Frankfurt am Main)

- Yuki Chiba (JAIST)
- Horatiu Cirstea (LORIA, Université de Lorraine, France)
- Santiago Escobar (Universitat Politècnica de València)
- Naoki Nishida (Nagoya University)
- David Sabel (Goethe-University Frankfurt am Main)
- Manfred Schmidt-Schauß (Goethe-University Frankfurt am Main)

Last modified 2017/08/16 by D. Sabel