IFIP Working Group 1.6: Term Rewriting

June 28, 2015 - Warsaw, Poland

Date

The date for WG 1.6 is Sunday, June 28, 2015. WG 1.6 will be part of RDP and it will take place on the day before RDP.

Aims

• To support the development of rewriting in particular and the study of formal structures in computations and deductions in general.
• To expand on the awareness and success of rewriting and lambda calculus in theoretical computer science.
• Represent and seek cooperations between all communities working on formal structures in computations and deductions.
• To foster development of applications of theoretical advances.

Invited Speakers

• Takahito Aoto.
  Proving Ground Confluence of Term Rewriting Systems by Rewriting Induction with Non-Orientable Equations
  Abstract: Ground confluence of term rewriting systems guarantees that all ground terms are confluent. Not confluence but ground confluence often matters in applications where not the equational validity but the inductive validity is of concern. Recently, interests for proving confluence of term rewriting systems automatically have been grown, and confluence provers have been developed. In contrast, it seems that little interests have been paid on developing tools for proving ground confluence automatically. In this talk, present a theoretically simple approach for proving ground confluence of term rewriting systems based on rewriting induction with non-orientable equations, and report on development of a ground confluence prover.
• Gilles Dowek.
  Polarization and Reachability
  Abstract: Polarized sequent calculus modulo theory led us to introduce polarized rewrite systems, where rules are classified into two categories : negative and positive. I will defend in this talk that this notion of polarized rewrite system is interesting in itself. As an example, I will present a method developed jointly with Guillaume Burel and Ying Jiang to decide reachability in various rewrite systems.
• Stéphane Graham-Lengrand.
  Non-idempotent Intersection Types and Quantitative Information about Reduction Paths: A Survey
  Abstract: Over the recent years, a new area in the study of intersection types has been explored. In the original spirit of intersection types, a term is of type A /\ B if it is both of type A and of type B, which naturally leads to an idempotent view of intersections: A /\ A is the same type as A. Dropping this idempotency property of intersections allows the design of resource-aware type systems, with deep connections to linear logic. This enriches typing with quantitative information about the lengths of reduction paths from typed terms. Upper bounds for these lengths -or even sometimes exact characterisations- have been provided by such typing systems, for various abstract machines and reduction strategies in the lambda-calculus and some of its variants. Among these, explicit substitution calculi proved a particularly appropriate approach to establishing such results. We will review this line of research, where typing is brought much closer to operational and denotational semantics, and discuss the connections that it opened towards neighbouring areas.
• Luke Ong.
  Compositional Higher-Order Model Checking, and the Model Checking of Higher-type Böhm Trees

Participation

The meetings of the working group are public, with the single exception of the business meeting.

Chair and Secretary