WPTE 2021

8th International Workshop on Rewriting Techniques for Program Transformations and Evaluation

WPTE 2021 will be held online on July 18, 2021.
It is affiliated with FSCD 2021. The registration to FSCD 2021 is required to participate in WPTE 2021.

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 2020 held online was affiliated with FSCD-IJCAR 2020, WPTE 2019 in Dortmund was affiliated with FSCD 2019, 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

Program

All times are in Buenos Aires (GMT-3). Current Buenos Aires local time is ??:??:??.

  • 06:30 - 07:30 Keynote Talk 1 by Helmut Seidl (Technical University of Munich)
    • Tree Transducers for Verification video 🎦 abstact
      hide abstact
      In this talk I will review connections between variations of the equivalence problem for topdown deterministic tree transducers and verification problems for imperative and certain functional programs.
         While (macro) tree transducers themselves can be viewed as certain (simple, yet expressive) functional programs recursively operating on structured inputs, the relationship of their equivalence problem to the verification of invariants of imperative programs is, perhaps, not so obvious.
         In this talk, we will highlight some of these connections, in particular, with respect to inter-procedural verification of imperative programs.
  • 07:30 - 08:00 Virtual coffee break
  • 08:00 - 10:00
    • Operationally-based Program Equivalence Proofs using LCTRSs (Ștefan Ciobâcă, Dorel Lucanu and Andrei Sebastian Buruiană) video 🎦 paper 📄 abstact
      hide abstact
      We propose an operationally-based framework for deductive proofs of program equivalence. It is based on encoding the language semantics as logically constrained term rewriting systems (LCTRSs) and the two programs as terms.
         Our method requires an extension of standard LCTRSs with axiomatized symbols. We also present a prototype implementation that proves the feasibility our approach.
    • Complexity of Deciding Syntactic Equivalence up to Renaming for Term Rewriting Systems (Michael Christian Fink Amores and David Sabel) video 🎦 paper 📄 abstact
      hide abstact
      Inspired by questions from program transformations, eight notions of isomorphisms between term rewriting systems are defined, analysed and classified. The notions include global isomorphisms where the renaming of variables and / or function symbols is the same for all term rewriting rules of the system, and local ones where a single renaming for every rule is used. The complexity of the underlying decision problems are analysed and either shown to be efficiently solvable or proved to be complete for the graph isomorphism complexity class.
    • On Transforming Inductive Definition Sets into Term Rewrite Systems (Shujun Zhang and Naoki Nishida) video 🎦 paper 📄 abstact
      hide abstact
      In this paper, we transform an inductive definition set—a set of productions for inductive predicates—into a term rewrite system (TRS, for short) such that a quantifier-free sequent over the first-order logic with the inductive definition set is valid if and only if its corresponding equation is an inductive theorem of the TRS. The resulting TRS is composed of three parts: Rewrite rules for logical connectives and a binary symbol for sequents; rewrite rules for productions; rewrite rules for the co-patterns of the second part. For correctness of the resulting TRS, we assume a certain property of the inductive definition set, which is a sufficient condition for ground termination and ground confluence of the resulting TRS. The transformation aims at comparing cyclic proof systems and rewriting induction.
    • Program Equivalence in Sequential Core Erlang (Dániel Horpácsi, Péter Bereczky and Simon Thompson) video 🎦 paper 📄 abstact
      hide abstact
      Our research aims to reason about the correctness of refactoring transformations of Erlang programs. As a stepping stone, we have developed formal semantics for sequential Core Erlang in the Coq proof assistant and we investigate reasoning about program transformations in Core Erlang. By refactoring, we mean program transformations that are expected to preserve the observable behaviour of programs. This property is characterised by a behavioural equivalence relation defined over the formal definition of semantics.
         In this paper, we adapt fundamental formalisations of expression equivalence to a Core Erlang subset, ranging from the simplest behavioural equivalence to logical relations and contextual equivalence. We examine the properties of these equivalence definitions and formally establish connections among them. The results are implemented in the Coq proof assistant.
  • 10:00 - 10:30 Virtual coffee break
  • 10:30 - 11:30 Keynote Talk 2 by Francisco Durán (ITIS Software, University of Málaga)
    • Maude support for the simulation and analysis of BPMN business processes abstact
      hide abstact
      A business process is a collection of structured activities producing a particular product or software. BPMN is a graphical notation for specifying business processes. Formally analyzing such processes is a crucial challenge in order to avoid erroneous executions of the corresponding software, and even if correct, their optimization with respect to multiple parameters is a key issue for current industrial practice. In this talk, I will journey through our different contributions in this regard using the rewriting-based tools available in Maude, including model checking, SMT solving, and simulation-based verification and analysis.
  • 11:30 - 12:15
    • Proving Renaming for Haskell via Dependent Types: A Case-Study in Refactoring Soundness (Adam Barwell, Christopher Brown and Susmit Sarkar) video 🎦 paper 📄 abstact
      hide abstact
      We present a formally verified renaming refactoring for a subset of Haskell 98 giving a case-study in proving soundness properties of Haskell refactorings. Our renaming is implemented in the dependently-typed language Idris, which allows us to encode soundness proofs as an integral part of the implementation. We give the formal definition of our static semantics for our Haskell 98 subset, which we encode as part of the AST, ensuring that only well-formed programs may be represented and transformed. This forms a foundation upon which refactorings can be formally specified. We then define soundness of refactoring implementations as conformity to their specification. We demonstrate our approach via renaming, a canonical and well-understood refactoring, giving its implementation alongside its formal specification and soundness proof.
    • Short talk: Towards a Maude framework for the analysis of smart contracts (Adrian Riesco) video 🎦 abstact
      hide abstact
      The popularity of blockchain technologies, which provide a distributed and decentralized mechanism for storing, retrieving, and verifying information, has stimulated the design and application of smart contracts. Smart contracts are just programs written in a particular programming language for automatically verifying some conditions and executing the corresponding actions if they hold (e.g. pay a bet to all winners). When executed in combination with a blockchain, smart contracts provide, a priori, a safe mechanism (in the sense that they do not depend on external agents and cannot be modified) for executing transactions. However, the immutability of the information stored in the blockchain makes analysis techniques critical for deployment, because we need to verify that the contracts have the expected behavior and consume the expected resources in advance.
         Maude is a high-performance logical framework based in rewriting logic where the semantics of different programming languages can be defined by means of rewrite rules. Because Maude specifications are executable, defining the semantics in Maude also provides an interpreter for free, making Maude a good candidate for prototyping. Moreover, Maude provides a powerful meta-level where Maude modules and terms can be used as usual data, hence allowing specifiers to reason about both the programming languages whose semantics has been defined in Maude (e.g. programming language L) and the programs written for these languages (e.g. smart contracts written in L).
         In this paper we propose a Maude framework where different smart contract languages can be parsed, executed, and analyzed. While the parsing and execution stages require a language-specific implementation, the analysis stage can be parameterized by the semantics, so it can be easily instantiated for different languages.

Paper Selection and Proceedings

Contributions to WPTE 2021

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. All submissions will be electronic via https://easychair.org/conferences/?conf=wpte2021.

Formal Proceedings

WPTE post-proceedings of selected papers will be published in a JLAMP special issue. For this, full papers must be submitted until the post-proceedings deadline. The authors of selected 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. The submission deadline for these post-proceedings will be after the workshop in September 2021. There will be a second round of reviewing for selecting papers to be published in the formal proceedings.

Important Dates

Program Committee

Steering Committee

Contact

All questions about submissions should be emailed to wpte2021 (at) easychair.org