Term Equivalence and Applications (TEA) Seminar

The TEA seminar is an online seminar between groups in Nijmegen, Amsterdam and Nagoya. We discuss methods to prove equivalence of term rewriting systems, or program equvialence using term rewriting systems.

Events:

• Tuesday 19 November 2024, 09:30 (Amsterdam/Nijmegen time) / 17:30 (Nagoya time)
  Speaker: Kasper Hagens
  Title: Program equivalence for Logically Constrained Term Rewriting Systems
  Abstract: Logically Constrained Term Rewriting Systems (LCTRSs) provide a framework very suitable for modeling both imperative and functional languages. One may convert programs in traditional languages into LCTRSs, and then use methods from term rewriting to analyze properties such as termination or program equivalence. In particular in functional programming, higher-order constructs arise naturally. These can be represented in higher-order term rewriting. Recent definition of LCSTRSs combines higher-order rewriting with logical constraints, which allows us to closely model functional programs. However, very few methods for their analysis have thus far been defined. In this presentation, I discuss program equivalence for LCSTRSs, combining the definition of rewriting induction for first-order constrained rewriting with insights from unconstrained higher-order equivalence analysis.
• Tuesday 14 November 2023, 09:00 (Amsterdam/Nijmegen time) / 17:00 (Nagoya time)
  Speaker: Naoki Nishida
  Title: On Transforming C Programs with Pointers into LCTRSs with Separation Logic
  Abstract: In this talk, I introduce an idea of transforming C programs with pointers into LCTRSs with Separation Logic (SL-LCTRS). I first propose SL-LCTRSs used for modeling heaps in configurations of imperative programs. Then, referring to some inference rules of semantics, I show an example of transforming a small C program with pointers into an SL-LCTRS.
• Friday 28 April 2023, 09:00 (Amsterdam/Nijmegen time) / 16:00 (Nagoya time)
  Speaker: Kasper Hagens
  Title: Matrix Invariants for program equivalence in LCTRSs
  Abstract: LCTRSs can be used as a formal language to prove program equivalence. A successful proof often requires the introduction of an invariant. We discuss a new method for automatically generating such invariants by using matrix calculations.
• Monday 20 March 2023, 09:00 (Amsterdam/Nijmegen time) / 17:00 (Nagoya time)
  Speaker: Misaki Kojima
  Title: From Starvation Freedom to All-Path Reachability Problems in Constrained Rewriting
  Abstract: An all-path reachability problem of a logically constrained term rewrite system is a pair of constrained terms representing state sets, and is demonically valid if every finite execution path from any state in the first set to a terminating state includes a state in the second set. We have proposed a framework to reduce the non-occurrence of specified error states in a transition system represented by a logically constrained term rewrite system to an all-path reachability problem of the system. In this talk, we extend the framework to verification of starvation freedom of asynchronous integer transition systems with shared variables such that some processes enter critical sections.
• Tuesday 10 January 2023, 09:00 (Amsterdam/Nijmegen time) / 17:00 (Nagoya time)
  Speaker: Liye Guo and Cynthia Kop
  Title: Higher-order LCTRSs
  Abstract: In this presentation, Cynthia will first presents thoughts and considerations for designing a higher-order rewriting formalism that is both general enough to express the things we need, and practical to analyse. Following this introduction, Liye will present a concrete definition of an applicative higher-order extension of LCTRSs (with types, but without abstraction).
• Tuesday 22 November 2022, 09:00 (Amsterdam/Nijmegen time) / 17:00 (Nagoya time)
  Speaker: Naoki Nishida
  Title: Equivalence Verification via Transformation of Programs into LCTRSs
  Abstract: In this talk, I first introduce my researches on constrained rewriting, together with an initial motivation (academic applications) and recent motivations (industrial applications). Then, I list LCTRS researches in the last decade: the proposal in 2013, an application to equivalence verification, Ctrl, and related work on LCTRSs, including on-going works in my group. Finally, I explain the progress of a common file format for LCTRSs, which is an on-going work of ARI project.