WRLA 2024

Luxembourg city. Photo by Manu on Unsplash

Topics of Interest

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.
  6. Education
    • how to design a course in which programming, formal specification, formal verification, etc. with Maude, Elan, CafeOBJ, etc. are taught
    • examples used in such courses
    • how to attract students for such courses
    • any issues related to such courses

Paper submissions

The program of the workshop will include regular papers, tool papers, education papers, and work-in-progress presentations.

Regular papers must contain original contributions, be clearly written, include appropriate references, and comparison with related work.

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 may be made available via the web.

Some of us have courses in which Maude, Elan, CafeOBJ, etc. are taught or used to teach formal methods, etc. We have not known what related courses are delivered, what examples are used in such courses, etc. Thus, the workshop is a time to share some ideas, tips, etc. for teaching Maude, Elan, and CafeOBJ. Education papers could contain how to design a course in which formal methods, etc. are taught with Maude, Elan, CafeOBJ, etc., what examples are used in such courses, etc.

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.

All submissions should be formatted according to the guidelines for Springer LNCS papers, and should not exceed 16 pages (for regular papers), 10 pages (for tool and education papers), and 8 pages (for work-in-progress presentations) excluding bibliography. Please carefully read Information for Authors of Springer Computer Science Proceedings when preparing your papers. Note that the ORCID of each author should be included in your papers. Submissions must be uploaded to the following EasyChair website: https://easychair.org/conferences/?conf=wrla2024.

  • Paper submission due: January 15  January 29  February 12, 2024 (AoE)
  • Notification: February 26  March 11, 2024
  • Camera-ready: March 11, 2024 (AoE)
  • Camera-ready for informal pre-proceedings: March 11  March 22, 2024 (AoE)
  • Camera-ready for formal LNCS post-proceedings: May 19, 2024 (AoE)


All accepted papers will be presented at the workshop and included in the pre-proceedings, which will be available during the workshop. Following the tradition of the last editions, regular, tool, and invited papers will be published as a volume in Springer's Lecture Notes in Computer Science (LNCS) series to be distributed after the workshop.