WPTE 2019

Sixth International Workshop on Rewriting Techniques for Program Transformations and Evaluation

Affiliated with FSCD 2019 in Dortmund, Germany.

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.

Previous Editions

WPTE 2018 in Oxford was affiliated with FLoC 2018 and FSCD 2018, WPTE 2017 in Oxford was affiliated with FSCD 2017, WPTE 2016 in Porto was affiliated with FSCD 2016, WPTE 2015 in Warsaw was affiliated with RDP 2015, and WPTE 2014 in Vienna was affiliated with RTA/TLCA 2014.

Topics of Interest


08:00-9:00 Registration
9:00-10:00 Session 1 (chair: Vivek Nigam)
Invited Talk: External Termination Proofs for Isabelle/HOL.

René Thiemann, University of Innsbruck


Isabelle/HOL is a logic that permits to write functional programs, and to specify and verify properties thereof. For recursive programs, usually termination must be proven. This can be done by either using Isabelle's internal automated termination prover, or by manually providing the termination argument.

In this talk, we consider a third possibility: the invocation of external termination tools in combination with the reconstruction of the resulting termination proofs within Isabelle. We discuss an existing approach via a program transformation to first-order rewriting, extend it to higher-order, illustrate its limits, and provide an outlook on some alternative approaches.

10:00-10:30 Coffee break
10:30-11:30 Session 2 (chair: David Sabel)
Space Improvements for Total Garbage Collection.

Manfred Schmidt-Schauss and Nils Dallmeyer


The focus of this paper are space-improvements of programs, which are transformations that do not worsen the space requirement during evaluations. A realistic theoretical treatment must take garbage collection method into account. We investigate space improvements under the assumption of an optimal garbage collector. Such a garbage collector is not implementable, but there is an advantage: The investigations are independent of potential changes in an implementable garbage collector and our results show that the evaluation and other similar transformations are space-improvements.

On Determinization of Inverted Grammar Programs via Context-Free.

Naoki Nishida and Minami Niwa


In this paper, we propose a determinization method of inverted grammar programs by means of context-free expressions which are straightforward extensions of regular expressions to context-free languages. Grammar programs are context-free grammars that an inversion method proposed by Glueck and Kawabe uses as intermediate results. We use conditional term rewriting systems (CTRSs, for short) as target programs, and our determinization method aims at transforming a given CTRS into a non-overlapping one that is semantically equivalent to the given one. To this end, we first translate a grammar program into an equivalent context-free expression. Then, by using some simple equalities of expressions, we transform the expression to a desired form. Finally, we translate the resulting expression back into an equivalent grammar program which can be translated back into a non-overlapping CTRS.

11:30-12:30 Session 3 (chair: ??)
Invited Talk: Strategic Graph Rewriting in an Interactive Modelling Framework.

Maribel Fernandez, King's College London


In this talk I will describe the use of strategic port graph rewriting as a basis for the implementation of visual modelling tools. The goal is to facilitate the specification and analysis of complex systems, in particular programs. A system is represented by an initial graph and a collection of graph rewrite rules, together with a user-defined strategy to control the application of rules.

The traditional notions of strategies for functional languages and term-rewriting languages have been adapted to deal with the more general setting of graph rewriting, and some new constructs have been included in the strategy language to deal with graph traversal and management of rewriting positions in the graph. We give a formal semantics for the language, examples of application, and a brief description of its implementation: the graph transformation and visualisation tool PORGY.

12:30-14:00 Lunch Break
14:00-15:30 Session 4 (chair: Naoki Nishida)
Invited Talk: SQL for combinatorial optimization problems and SMT-based solving by SQL transformation.

Masahiko Sakai, Nagoya University


Combinatorial optimization is an important topic, which finds an optimal solution from finite objects. This talk presents an description language for combinatorial optimization problems (COPs) and a solution method powered by state-of-the-art SMT solvers.

A COP is determined by (i) a set of objects, called a search space, (ii) a predicate on the objects deciding solutions, and (iii) a goal function defining the optimality. The description language is designed based on the structural query language (SQL). (i) A search space is defined by an extended syntax of SQL, like as all functions between two sets, each of which is given by a relational-database table. (ii) A predicate is given as a Boolean SQL query. (iii) A goal function is given as an integer SQL query.

Toward an effective implementation, the search space consisting of relations is represented by a relational table containing variables over finite domains. The predicate (the goal function) is converted into SMT constraints over the introduced variables. This enables us to solve the target problem by SMT solvers. To this end, we developed an SQL transformation technique, where an execution of the resulted SQL query by an existing SQL-engine generates quantifier free linear integer arithmetic (QFLIA) constraints. A key idea is the use of user-definable functions that may cause side-effects allowed in the database system SQLite. As a result, we successfully give an simple implementation without developing a complex extended SQL-engine. Moreover, our implementation allows full-SQL query facilities in the SQL-based COP specifications.

15:30-16:00 Coffee Break
16:00-17:00 Session 5 (chair: ???)
Formalisation of Normalisation of the Simply Typed Lambda Calculus in F*.

Sebastian Sturm


As the implementations of program transformations grow in size and complexity, the importance of formal correctness arguments rises. One option is a formal verification using interactive theorem provers. POPLmark-Reloaded is a theorem prover challenge from the field of programming meta-theory, precisely normalisation for the simply typed lambda calculus (STLC), and as such particularly suited for testing theorem provers on that field.

This paper presents a partial solution for the POPLmark-Reloaded challenge in F*. F* is a dependently typed programming language usable both for verification and as a proof assistant. It combines interactive proving with automatic, SMT based, approaches. After a short introduction to F* and an overview for POPLmark-Reloaded we will describe the formalisation and some benefits and drawbacks of using F* for programming meta-theory proofs.

On Formalizing a Transformation of IMP Programs into Logically Constrained Term Rewriting Systems in Isabelle/HOL.

Ryota Nakayama and Naoki Nishida


In this paper, we aim at formalizing a transformation of an IMP program into a logically constrained term rewriting system (LCTRS, for short) in Isabelle/HOL. To this end, we formalize LCTRSs and the transformation in Isabelle/HOL.

Invited Speakers

Program Committee

Paper Selection and Proceedings

Contributions to WPTE 2019

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. 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/). Extended abstract submission to WPTE'2019 is handled by easychair at https://easychair.org/conferences/?conf=wpte2019.

Formal Proceedings

As in previous years, we intend to publish WPTE post-proceedings of selected papers by the Electronic Proceedings in Theoretical Computer Science. For this, full papers must be submitted until the post-proceedings deadline. The authors of all presented contributions will have the opportunity (but no obligation) to submit a full paper for the formal post-proceedings. These 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 September 2018. There will be a second round of reviewing for selecting papers to be published in the formal proceedings.

Important Dates

Steering Committee