View: session overviewtalk overviewside by side with other conferences

08:30-09:00Coffee & Refreshments
09:00-10:30 Session 26C: Confluence criteria and completeness
Location: Ullmann 306
Development Closed Critical Pairs: Towards a Formalized Proof
PRESENTER: Aart Middeldorp

ABSTRACT. Having development closed critical pairs is a well-known sufficient condition for confluence of left-linear term rewrite systems. We present formalized results involving proof terms and unification that play an important role in the proof.

On Confluence of Parallel-Innermost Term Rewriting
PRESENTER: Carsten Fuhs

ABSTRACT. We revisit parallel-innermost term rewriting as a model of parallel computation on inductive data structures. We propose a simple sufficient criterion for confluence of parallel-innermost rewriting based on non-overlappingness. Our experiments on a large benchmark set indicate the practical usefulness of our criterion. We close with a challenge to the community to develop more powerful dedicated techniques for this problem.

Uniform Completeness

ABSTRACT. We introduce uniform completeness and give a local characterisation of it. We show it yields a complete method for showing completeness of rewrite systems.

10:30-11:00Coffee Break
11:00-12:30 Session 31D: Invited talk and equivalence
Location: Ullmann 306
Seven Confluence Criteria for Solving COPS #20

ABSTRACT. COPS #20 is a thought-provoking confluence problem for term rewriting, posed by Gramlich and Lucas (2006). Although the term rewrite system of the problem is confluent, it is beyond the realm of classical confluence criteria such as Knuth and Bendix' criterion (1970) and Huet's parallel closedness (1980). In this talk we will discuss various solutions to the problem, recalling powerful confluence methods developed in the last decade and a half.

Formalized Signature Extension Results for Equivalence

ABSTRACT. Conversion equivalence and normalization equivalence are important properties of two rewrite systems. We investigate how many constants are needed to reduce these properties to their ground versions for linear variable-separated rewrite systems. Our results are implemented in the decision tool FORT-h and formalized in Isabelle/HOL. The latter enables the validation of the proofs produced by the former in the certifier FORTify.

12:30-14:00Lunch Break

Lunches will be held in Taub hall and in The Grand Water Research Institute.

14:00-15:30 Session 34E: Conditional rewriting
Location: Ullmann 306
On local confluence of conditional rewrite systems

ABSTRACT. We characterize local confluence of *conditional rewrite systems* à la Huet, i.e., as the joinability of a set of conditional pairs including the usual conditional critical pairs and a new kind of pairs we call *conditional variable pairs*.

A Critical Pair Criterion for Level-Commutation of Conditional Term Rewriting Systems
PRESENTER: Takahito Aoto

ABSTRACT. We introduce level-commutation of conditional term rewriting systems (CTRSs) that extends the notion of level-confluence, in a way similar to extending confluence to commutation. We show a criterion for level-commutation of oriented CTRSs, which generalizes the one for commutation of term rewriting systems in (Toyama, 1987). As a corollary, we obtain a criterion of level-confluence of oriented CTRSs which extends the one in (Suzuki et al., 1995).

Proving Confluence with CONFident
PRESENTER: Raúl Gutiérrez

ABSTRACT. This paper describes the proof framework used in CONFident, a framework to deal with different types of systems (term rewriting systems, context-sensitive term rewriting systems and conditional term rewriting systems) and different types of tasks (checking joinability of critical pairs, termination of systems, feasibility of reachibility problems or deducibility) and different techniques for proving confluence (including modular decompositions, transformations, etc.).

15:30-16:00Coffee Break
16:00-18:00 Session 37E: Higher-order rewriting and CoCo
Location: Ullmann 306
Confluence by Higher-Order Multi--One Critical pairs with an application to the Functional Machine Calculus

ABSTRACT. We show all multi--one critical peaks being many--multi joinable entails confluence of positional pattern rewrite systems (PRSs). To apply this result to the functional machine calculus (FMC), we embed the FMC in a $3$rd order PRS and show its multi--one critical peaks to be one--multi joinable, regaining its (known) confluence via higher-order rewriting.

Checking Confluence of Rewrite Rules in Haskell

ABSTRACT. We present a tool GSOL, a confluence checker for GHC. It checks the confluence property for rewrite rules in a Haskell program by using the confluence checker SOL (Second-Order Laboratory). %Haskell is a non-strict and purely functional programming language. The Glasgow Haskell Compiler (GHC) allows the user to use rewrite rules to optimize Haskell programs in the compilation pipeline. Currently, GHC does not check the confluence of the user-defined rewrite rules. If the rewrite rules are not confluent then the optimization using these rules may produce unexpected results. Therefore, checking the confluence of rewrite rules is important. We implement GSOL using the plugin mechanism of GHC.

Confluence Competition
18:30-20:00Workshop Dinner (at the Technion, Taub Terrace Floor 2) - Paid event