View: session overviewtalk overviewside by side with other conferences
09:00  Confluence in Constraint Handling Rules: An overview from early, fundamental results to recent extensions including state invariants and conf. modulo equivalence. SPEAKER: Henning Christiansen ABSTRACT. Constraint Handling Rules, CHR, is a nondeterministic programming language whose programs consists of rewrite rules over program states, and being able to show confluence may be an important part of a program correctness proof. In fact, most CHR implementations are deterministic, yet confluence is useful as the programmer does not need to consider the details of the underlying execution strategy. The initial results on proving confluence in CHR, developed during to the 1990s, were formulated with respect to a logicbased semantics. This choice gave elegant proofs based on the Critical Pair Theorem and Newman's lemma but can only describe a limited class of programs, namely logical (and terminating) programs. It can be argued that invariants and confluence modulo equivalence are important from a practical point of view. Most programs are developed with a particular set of initial queries in mind, which reduces the set of reachable states. Therefore, taking the induced invariant into account makes a much larger class of programs confluent. Confluence modulo equivalence is a generalization where forked states must reach equivalent states, rather than a common state. For instance, a program may produce redundant data structures such as representing sets as lists, and the equivalence states that the order of the elements does not matter. Both the invariant and the equivalence relation may be tailored for the individual program. In our recent work, we have extended previous methods for proving confluence to include invariants and confluence modulo equivalence. We have focused on a more realistic semantics that reflects the defacto standard implementations of CHR upon Prolog, including a correct treatment of Prolog's nonlogical devices (e.g., var/1, nonvar/1, is/2) and runtime errors. As part of this, we developed a notion of abstract simulations that may be interesting also for other kinds of transition and rewriting systems. The classical critical pair constructions are generalized, having the transition system of interest simulated by another metalevel system (rather that reusing the system itself). This is useful especially for invariants and state equivalences that  by nature  are metalevel statements that typically cannot be expressed in the original system. 
10:00  Coherence modulo relations SPEAKER: Benjamin Dupont ABSTRACT. The computation of minimal convergent presentations for monoids, categories or higherdimensional categories appear in lowdimensional combinatorial problems on these structures, such as coherence problems. A method to compute coherent presentations using convergent string rewriting systems was developed following works of Squier. In this approach, coherence results are formulated in terms of confluence diagrams of critical pairs. This work proposes an extension of these methods to string rewriting systems modulo. 
11:00  Coherence of monoids by insertions SPEAKER: Nohra Hage ABSTRACT. We introduce string data structures as combinatorial descriptions of structured words on totally ordered alphabets. The data can be described by words through a reading map and can be constructed by using an insertion algorithm. The insertion map defines a product on datum. We show that the associativity of this product, the cross section property of the data structure, and the confluence of the rewriting system defined by the insertion map are equivalent properties. We explicit a coherent presentation of the monoid presented by the data structure, made of generators, rewriting rules describing the insertion of letters in words and relations among the insertion algorithms. 
11:30  Critical pairs for Gray categories ABSTRACT. Higher categories are a generalization of standard categories where there are not only $1$cells between $0$cells but more generally $n{+}1$cells between $n$cells. They are more and more used in mathematics, physics and computer science. They can notably be used to represent algebraic structures. There are several variants going from weak categories, that are the most general formalism but also the hardest to manipulate, to strict categories, simpler but less general. One usually wants both the expressive power of weak categories and the simplicity of strict categories. Semistrict categories, such as Gray categories in dimension $3$, are an inbetween formalism that it used in this work. Here, we are interested in proving \emph{coherence} of certain algebraic structures in dimension $3$ using rewriting, where ``coherence'' is the property that there is at most one $3$cell between two $2$cells. It amounts to compute critical pairs of a rewriting system and use a variant of Newmann's lemma. In this setting, an algorithm exists to compute these critical pairs. 
12:00  The diamond lemma for free modules ABSTRACT. We are studying rewriting systems over free modules, that is linear combinations of free generators with noninvertible coefficients. We provide a sufficient condition in terms of local confluence restricted to generators for the global rewrite relation to be confluent: this condition is formulated in terms of syzygies. When the coefficients belong to a domain, we equip the set of syzygies with a module structure, which provides a finer criterion: the local confluence has to be checked over a subset of syzygies, namely a generating set for the module structure. 
14:00  SPEAKER: Naoki Nishida ABSTRACT. Unravelings, which are transformations of a conditional term rewriting system (CTRS, for short) into an unconditional term rewriting system (TRS, for short), are useful to prove confluence and operational termination of some CTRSs. A simultaneous unraveling has been proposed for normal 1CTRSs and a sequential one has been proposed for deterministic 3CTRSs, the class of which includes normal 1CTRSs. In this paper, we first show that for a normal 1CTRS, the simultaneously unraveled TRS is orthogonal iff so is the sequentially unraveled one. Then, we show that for a normal 1CTRS, if the simultaneously unraveled TRS is terminating, then so is the sequentially unraveled one. Finally, we show that for a normal 1CTRS with termination of the unraveled TRS, the simultaneously unraveled TRS is locally confluent iff so is the sequentially unraveled one. 
14:30  SPEAKER: T. V. H. Prathamesh ABSTRACT. Confluence is a decidable property of ground rewrite systems. We present a formalization effort in Isabelle/HOL of the decision procedure based on ground tree transducers. 
15:00  Certified Ordered Completion SPEAKER: Sarah Winkler ABSTRACT. On the one hand, ordered completion is a fundamental technique in equational theorem proving that is employed by automated tools. On the other hand, their complexity makes such tools inherently error prone. As a remedy to this situation we give an Isabelle/HOL formalization of ordered rewriting and completion that comes with a formally verified certifier for ordered completion proofs. By validating generated proof certificates, our certifier increases the reliability of ordered completion tools. 
16:00  Complete Axiom System of Cluster Algebra SPEAKER: Kousuke Fukui ABSTRACT. Top trees with DAG representation can be used to compress huge orderedtree data such as XML documents. However, one ordered tree can be represented by several top trees, so it is necessary to efficiently decide which top trees represent the same tree for higher compression rate. In this paper, we give a complete axiom system for the equational theory of top trees, called the cluster algebra. In order to prove the completeness, we introduce a reduction system on cluster algebra, and show the strong normalization and the unique normal form property. 
16:30  SPEAKER: Aart Middeldorp ABSTRACT.

Workshops dinner at Balliol College. Drinks reception from 7.45pm, to be seated by 8:15 (prebooking via FLoC registration system required; guests welcome).