Workshop Description

Rewriting is a natural model of computation and an expressive semantic framework for concurrency, parallelism, communication, and interaction. It can be used for specifying a wide range of systems and languages in various application domains. It also has good properties as a metalogical framework for representing logics. Several successful languages based on rewriting (ASF+SDF, CafeOBJ, ELAN, Maude) have been designed and implemented. The aim of WRLA is to bring together researchers with a common interest in rewriting and its applications, and to give them the opportunity to present their recent work, discuss future research directions, and exchange ideas.

The topics of the workshop include, but are not limited to:
  1. Foundations
    • foundations and models of rewriting and rewriting logic, including termination, confluence, coherence, and complexity
    • unification, generalization, narrowing, and partial evaluation
    • constrained rewriting and symbolic algebra
    • graph rewriting
    • tree automata
    • rewriting strategies
    • rewriting-based calculi and explicit substitutions
  2. Rewriting as a Logical and Semantic Framework
    • uses of rewriting and rewriting logic as a logical framework, including deduction modulo
    • uses of rewriting as a semantic framework for programming language semantics
    • rewriting semantics of concurrency models, distributed systems, and network protocols
    • rewriting semantics of real-time, hybrid, and probabilistic systems
    • uses of rewriting for compilation and language transformation
  3. Rewriting Languages
    • rewriting-based declarative languages
    • type systems for rewriting
    • implementation techniques
    • tools supporting rewriting languages
  4. Verification Techniques
    • verification of confluence, termination, coherence, sufficient completeness, and related properties
    • temporal, modal, and reachability logics for verifying dynamic properties of rewrite theories
    • explicit-state and symbolic model checking techniques for verification of rewrite theories
    • rewriting-based theorem proving, including (co)inductive theorem proving
    • rewriting-based constraint solving and satisfiability
    • rewriting-semantics-based verification and analysis of programs
  5. Applications
    • applications in logic, mathematics, physics, and biology
    • rewriting models of biology, chemistry, and membrane systems
    • security specification and verification
    • applications to distributed, network, mobile, and cloud computing
    • specification and verification of real-time, hybrid, probabilistic, and cyber-physical systems
    • specification and verification of critical systems
    • applications to model-based software engineering
    • applications to engineering and planning.

Registration

The original dates of WRLA 2020 were April 25th and 26th, 2020 to be held in Dublin, Ireland. Due to COVID-19, the workshop, as well as other ETAPS 2020 events, were cancelled. The workshop will be held as an online event during three days, Tuesday October 20th to Thursday October 22nd, with different time zones for each day. All the talks are clearly marked with times in four timezones: Japan Standard Time (JST), Central European Summer Time (CEST), US Central Daylight Time (CDT), and US Pacific Daylight Time (PDT).

Attendance will be free but former registration will be required through this link. All events will be held using Microsoft Teams, which is available for different platforms including Windows, Mac and Linux and even through web browsers, in case you do not want to install any software. All the information necessary for connecting to the meetings will be sent by email to the registered participants.

Online Program

Tuesday October 20th, 2020

Welcome!!!
  8:50PM JST
  1:50PM CEST
  6:50AM CDT
  4:50AM PDT
René Thiemann (Invited talk)
From Rewriting to Algebra: Certifying Complexity Proofs with an Extended Perron-Frobenius Theorem (Video)
  9:40PM JST
  2:40PM CEST
  7:40AM CDT
  5:40AM PDT
Thierry Boy de La Tour and Rachid Echahed
Combining Parallel Graph Rewriting and Quotient Graphs (Video)
10:00PM JST
  3:00PM CEST
  8:00AM CDT
  6:00AM PDT
Break
10:10PM JST
  3:10PM CEST
  8:10AM CDT
  6:10AM PDT
Rubén Rubio, Narciso Marti-Oliet, Isabel Pita and Alberto Verdejo
Strategies, model checking and branching-time properties in Maude (Video)
10:30PM JST
  3:30PM CEST
  8:30AM CDT
  6:30AM PDT
Óscar Martín, Alberto Verdejo and Narciso Marti-Oliet
Compositional Verification in Rewriting Logic (Video)
10:50PM JST
  3:50PM CEST
  8:50AM CDT
  6:50AM PDT
Mircea Marin, Besik Dundua and Temur Kutsia
A Rule-based System for Computation and Deduction in Mathematica (Video)
11:10PM JST
  4:10PM CEST
  9:10AM CDT
  7:10AM PDT
Break
11:20PM JST
  4:20PM CEST
  9:20AM CDT
  7:20AM PDT
Jose Meseguer and Stephen Skeirik
Inductive Reasoning with Equality Predicates, Contextual Rewriting and Variant-Based Simplification (Video)
11:40PM JST
  4:40PM CEST
  9:40AM CDT
  7:40AM PDT
Vivek Nigam and Carolyn Talcott
Automated Construction of Security Integrity Wrappers for Industry 4.0 Applications (Video)

Wednesday October 21st, 2020

  0:50AM JST (+1 day)
  5:50PM CEST
10:50AM CDT
  8:50AM PDT
Steven Eker (Invited talk)
Associative Unification in Maude (Video)
  1:40AM JST (+1 day)
  6:40PM CEST
11:40AM CDT
  9:40AM PDT
Jose Meseguer
Variants in the Infinitary Unification Wonderland (Video)
  2:00AM JST (+1 day)
  7:00PM CEST
12:00PM CDT
10:00AM PDT
Break
  2:10AM JST (+1 day)
  7:10PM CEST
12:10PM CDT
10:10AM PDT
Jose Meseguer
Variant Satisfiability of Parameterized Strings (Video)
  2:30AM JST (+1 day)
  7:30PM CEST
12:30PM CDT
10:30AM PDT
Matthew Francis-Landau, Tim Vieira and Jason Eisner
Evaluation of Logic Programs with Built-Ins and Aggregation: A Calculus for Bag Relations (Video)
  2:50AM JST (+1 day)
  7:50PM CEST
12:50PM CDT
10:50AM PDT
Francisco Durán, Camilo Rocha and Gwen Salaün
Analysis of the Runtime Resource Provisioning of BPMN Processes using Maude (Video)
  3:10AM JST (+1 day)
  8:10PM CEST
  1:10PM CDT
11:10AM PDT
Break
  3:20AM JST (+1 day)
  8:20PM CEST
  1:20PM CDT
11:20AM PDT
Stephen Skeirik, José Meseguer and Camilo Rocha
Verification of the IBOS Browser Security Properties in Reachability Logic (Video)
  3:40AM JST (+1 day)
  8:40PM CEST
  1:40PM CDT
11:40AM PDT
Xiaohong Chen, Dorel Lucanu and Grigore Rosu
Connecting Constrained Constructor Patterns and Matching Logic (Video)

Thursday October 22nd, 2020

  1:50PM JST
  6:50AM CEST
11:50PM CDT (-1 day)
  9:50PM PDT (-1 day)
Mark-Oliver Stehr (Invited talk)
Learning with Knowledge: Initial Steps towards a Neuro-Symbolic Architecture based on Maude (Video)
  2:40PM JST
  7:40AM CEST
12:40AM CDT
10:40PM PDT (-1 day)
Mitsuhiro Okada and Yuta Takahashi
A Simplified Application of Howard's Vector Notation System to Termination Proofs for Typed Lambda-Calculus Systems (Video)
  3:00PM JST
  8:00AM CEST
  1:00AM CDT
11:00PM PDT (-1 day)
Kokichi Futatsugi
Well-Founded Induction via Term Refinement in CafeOBJ (Video)
  3:20PM JST
  8:20AM CEST
  1:20AM CDT
11:20PM PDT (-1 day)
Geunyeol Yu and Kyungmin Bae
Maude-SE: a Tight Integration of Maude and SMT Solvers (Video)
Wrap up and conclucions

Important Dates

  • Paper submission:
  • January 12th →January 26th, 2020
  • Author notification:
  • February 10th → March 8th, 2020
  • ETAPS Registration:
  • Until March 16th, 2020
  • Final version:
  • March 1st→ March 22nd, 2020
  • Workshop dates:
  • April 25-26th → October 20-22nd, 2020

    Call For Papers

    Available here.

    Accepted Papers

    • Thierry Boy de La Tour and Rachid Echahed. Combining Parallel Graph Rewriting and Quotient Graphs
    • Xiaohong Chen, Dorel Lucanu and Grigore Rosu. Connecting Constrained Constructor Patterns and Matching Logic
    • Francisco Durán, Camilo Rocha and Gwen Salaün. Analysis of the Runtime Resource Provisioning of BPMN Processes using Maude
    • Matthew Francis-Landau, Tim Vieira and Jason Eisner. An Execution Formalism for Dyna: Merging the best of Datalog and Prolog via a Term Rewriting Relational Algebra
    • Kokichi Futatsugi. Well-Founded Induction via Term Refinement in CafeOBJ
    • Mircea Marin, Besik Dundua and Temur Kutsia. A Rule-based System for Computation and Deduction in Mathematica
    • Óscar Martín, Alberto Verdejo and Narciso Marti-Oliet. Compositional Verification in Rewriting Logic
    • Jose Meseguer and Stephen Skeirik. Inductive Reasoning with Equality Predicates,Contextual Rewriting and Variant-Based Simplification
    • Jose Meseguer. Variants in the Infinitary Unification Wonderland
    • Jose Meseguer. Variant Satisfiability of Parameterized Strings
    • Mitsuhiro Okada and Yuta Takahashi. A Remark for the Use of a Path Ordering with an Algebra and a Howard-Style Interpretation of Lambda for Termination Proofs of Typed Rewrite Systems
    • Rubén Rubio, Narciso Marti-Oliet, Isabel Pita and Alberto Verdejo. Strategies, model checking and branching-time properties in Maude
    • Stephen Skeirik, José Meseguer and Camilo Rocha. Verification of the IBOS Browser Security Properties in Reachability Logic
    • Carolyn Talcott and Vivek Nigam. Automated Construction of Security Wrappers for Industry 4.0 Applications
    • Geunyeol Yu and Kyungmin Bae. Maude-SE: a Tight Integration of Maude and SMT Solvers

    Submission

    The program of the workshop will include regular papers, tool papers, and work-in-progress presentations. The program will also contain invited papers, and tutorials to be determined by the program committee.

    Regular papers must contain original contributions, be clearly written, include appropriate references, and comparison with related work. They must be unpublished and not submitted simultaneously for publication elsewhere.

    Tool papers have to present a new tool, a new tool component, or novel extensions to an existing tool. They should provide a short description of the theoretical foundations with relevant citations, emphasize the design and implementation, and give a clear account of the tool's functionality. The described tools must be available via the web.

    Work-in-progress papers present early-stage work or other types of innovative or thought-provoking work related to the topics of the workshop. The difference between work-in-progress and regular papers is that work-in-progress submissions represent work that has not reached yet a level of completion that would warrant the full refereed selection process. We encourage researchers and practitioners to submit work-in- progress papers as this provides a unique opportunity for sharing valuable ideas, eliciting useful feedback on ongoing work, and fostering discussions and collaborations among colleagues.

    All submissions should be formatted according to the guidelines for Springer LNCS papers and should not exceed 15 pages including references. Papers must be submitted electronically as a PDF file using the EasyChair system.

    Publication

    All submissions will be evaluated by the program committee. Regular papers, tool papers, and work-in-progress papers that are accepted will be presented at the workshop and included in the pre-proceedings, which will be available during the workshop are available online here. Following the tradition of the last editions, regular papers, tool papers, and invited presentations will be has been published as a volume in Springer's Lecture Notes in Computer Science (LNCS) series to be distributed after the workshop available here.

    A special issue of JLAMP, the Journal of Logical and Algebraic Methods in Programming, is approved for extended versions of selected papers from WRLA 2020.

    Best Paper Award

    The program committee will consider a best paper award (a diploma and 500 €) for a paper in which at least one author is a junior researcher (a PhD student or the PhD defense was less than two years ago). The PC chairs may require the other authors to declare that at least 50% of the contribution was made by the junior researcher.

    The best paper award has been given to Xiaohong Chen.

    Program Committee

    • Erika Abraham - RWTH Aachen, Germany
    • María Alpuente - Universitat Politècnica de València, Spain
    • Irina Mariuca Asavoae - Trusted Labs, France
    • Kyungmin Bae - Pohang University of Science and Technology, Korea
    • Clara Bertolissi - Aix-Marseille University, France
    • Artur Boronat - University of Leicester, United Kingdom
    • Roberto Bruni - Università di Pisa, Italy
    • Francisco Durán - Universidad de Málaga, Spain
    • Santiago Escobar - Universitat Politècnica de València, Spain (co-chair)
    • Maribel Fernández - King's College London, United Kingdom
    • Thomas Genet - Université de Rennes, France
    • Raúl Gutiérrez - Universitat Politècnica de València, Spain
    • Nao Hirokawa - JAIST, Japan
    • Alexander Knapp - University Augsburg, Germany
    • Alberto Lluch-Lafuente - Technical University of Denmark, Denmark
    • Dorel Lucanu - Alexandru Ioan Cuza University, Romania
    • Narciso Martí-Oliet - Universidad Complutense de Madrid, Spain (co-chair)
    • Aart Middeldorp - University of Innsbruck, Austria
    • José Meseguer - University of Illinois at Urbana-Champaign, USA
    • Cesar A. Muñoz - NASA Langley Research Center, USA
    • Vivek Nigam - Federal University of Paraíba, Brazil
    • Etienne Payet - University of La Reunion, France
    • Kazuhiro Ogata - JAIST, Japan
    • Adrián Riesco - Universidad Complutense de Madrid, Spain
    • Christophe Ringeissen - INRIA, France
    • Camilo Rocha - Pontificia Universidad Javeriana, Colombia
    • Grigore Rosu - University of Illinois at Urbana-Champaign, USA
    • Vlad Rusu - INRIA Lille, France
    • Ralf Sasse - ETH Zurich, Switzerland
    • Traian Serbanuta - University of Bucharest, Romania
    • Carolyn Talcott - SRI International, USA

    Steering Committee

    • Kokichi Futatsugi, JAIST, Japan
    • Claude Kirchner, INRIA Research Center Bordeaux - Sud-Ouest, France
    • Narciso Martí-Oliet, Universidad Complutense de Madrid, Spain
    • José Meseguer, University of Illinois at Urbana-Champaign, USA
    • Ugo Montanari, University of Pisa, Italy
    • Grigore Rosu, University of Illinois at Urbana-Champaign, USA
    • Carolyn Talcott, SRI International, USA
    • Martin Wirsing, Ludwig Maximilians Universität München, Germany