10th International Workshop on Confluence
23rd July 2021, online
(originally: Buenos Aires, Argentina)
Colocated with FSCD
Confluence provides a general notion of determinism and has been conceived as one of the central properties of rewriting systems. Confluence relates to many topics of rewriting (completion, modularity, termination, commutation, etc.) and has been investigated in many formalisms of rewriting, such as first-order rewriting, lambda-calculi, higher-order rewriting, constraint rewriting, conditional rewriting, and so on. Recently there is a renewed interest in confluence research, resulting in new techniques, tool support, confluence competition, and certification as well as in new applications. The scope of the workshop is all these aspects of confluence and related topics.
The goal of the workshop is to provide a forum for researchers interested in the topic of confluence to exchange and share new developments in the field. The workshop will enable discussion on theoretical results, new problems, applications, implementations and benchmarks, and share the current state-of-the-art on the development of confluence tools.
The 10th Confluence Competition CoCo 2021 will run live during IWC 2021.
- confluence and related properties (unique normal forms, commutation, ground confluence)
- critical pair criteria
- decidability issues
- complexity issues
- system descriptions
- applications of confluence
- submission (abstract): Monday, April 19th, 2021
- submission (paper): Monday, April 26th, 2021
- notification: Monday, May 31st, 2021
- final version: Monday, June 14th, 2021
- workshop: Friday, July 23rd, 2021
- submission (paper): Monday, April 26th, 2021
(deadlines are AoE)
The proceedings are available online and include reports on the 10th Confluence Competition. You can also find individual papers below:
- Vincent van Oostrom: Multi-redexes and multi-treks induce residual systems; least upper bounds and left-cancellation up to homotopy
- Lars Hellström: Wrap ambiguities and how to enumerate them
- Benjamin Dupont, Philippe Malbos and Isaac Ren: Completion of operadic rewriting systems by Gaussian elimination
- Alexander Lochmann, Fabian Mitterwallner and Aart Middeldorp: Formalized Signature Extension Results for Confluence, Commutation and Unique Normal Forms
- Claudia Faggian, Giulio Guerrieri and Riccardo Treglia: Evaluation in the computational calculus is non-confluent
- Andrew Kenyon-Roberts: A Confluent Trace Semantics for Probabilistic Lambda Calculus
- Uran Meha: Confluence in string rewriting systems compatible with a crystal structure
All times are indicated in GMT-3 (= time in Buenos Aires).
06:30 - 07:30 Jesper Cockx: The quest for modular confluence of rewrite rules in type theory 07:30 - 08:00 Break 08:00 - 08:30 Vincent van Oostrom: Multi-redexes and multi-treks induce residual systems; least upper bounds and left-cancellation up to homotopy 08:30 - 09:00 Andrew Kenyon-Roberts: A Confluent Trace Semantics for Probabilistic Lambda Calculus 09:00 - 09:30 Claudia Faggian, Giulio Guerrieri and Riccardo Treglia: Evaluation in the computational calculus is non-confluent 09:30 - 10:00 Benjamin Dupont, Philippe Malbos and Isaac Ren: Completion of operadic rewriting systems by Gaussian elimination 10:00 - 10:30 Break 10:30 - 11:30 10th Confluence Competition - CoCo 2021 11:30 - 12:00 Alexander Lochmann, Fabian Mitterwallner and Aart Middeldorp: Formalized Signature Extension Results for Confluence, Commutation and Unique Normal Forms 12:00 - 12:30 Break 12:30 - 13:30 José Meseguer: Proving Ground Confluence of Equational Programs 13:30 - 14:00 Uran Meha: Confluence in string rewriting systems compatible with a crystal structure 14:00 - 14:30 Lars Hellström: Wrap ambiguities and how to enumerate them
- Jesper Cockx (TU Delft) The quest for modular confluence of rewrite rules in type theory
Dependent type theory provides a powerful foundation for proof assistants and programming languages such as Coq and Agda. To overcome some of the limitations of those systems and to improve their usability, we can extend them with user-defined rewrite rules. However, these rewrite rules can easily break important properties of the type theory, in particular subject reduction (i.e. type preservation) and decidability of type checking. To regain these properties, we need a criterion to ensure the confluence of the user-provided rewrite rules. In order to be practicably usable, this criterion should be modular: different modules should be able to be combined without additional checks. It should also ensure *global* confluence, even in the presence of non-terminating rules. And finally, it should be simple enough to allow formal verification of its correctness.
In this talk, I will present our quest for a confluence criterion satisfying all of these requirements. This quest lead us back in history to the classic proof of confluence of untyped lambda calculus by Tait and Martin-Löf, which makes use of the triangle property of parallel reduction. Based on this triangle property we designed Rewriting Type Theory (RTT), a type theory with user-defined rewrite rules and a modular and decidable criterion for global confluence. The properties of RTT have been formally verified using the MetaCoq framework and it has been implemented as an extension to the Agda proof assistant.
- José Meseguer (University of Illinois at Urbana-Champaign) Proving Ground Confluence of Equational Programs
A declarative functional program can be naturally specified as a, possibly conditional, equational theory. The equations in the program, oriented as rewrite rules, should of course have a deterministic behavior. What this really means is that such rules should be ground confluent. Paradoxically, proving the stronger property of confluence is much easier than proving ground confluence. But there are perfectly correct and natural programs that are not confluent and cannot be made so: any attempt to complete their rewrite rules would generate an infinite set of rules. This is not a "black swan" occurrence, but a relatively common fact of life in actual practice. This poses a challenge, not only for checking the deterministic nature of a functional program, but also for theorem proving verification of its properties.
This talk will report on some recent methods for proving ground confluence of possibly conditional equational programs that I have been developing with several colleagues in the context of verifying properties of functional modules in Maude, that is, functional programs that are equational theories in order-sorted equational logic. Since (1) the rules can be conditional; (2) order-sorted logic contains many-sorted and unsorted logics as special cases; and (3) rewriting is performed modulo any combination of associativity and/or commutativity and/or identity axioms, these methods apply to a very general class of theories, are language-independent, and should be of interest for reasoning about equational programs in many language.
- Beniamino Accatolli (Inria & LIX, École Polytechnique)
- Sandra Alves (Universidade do Porto)
- Cyrille Chenavier (Université de Limoges)
- Francisco Durán (University of Málaga)
- Alejandro Díaz-Caro (Universidad Nacional de Quilmes & ICC/UBA-CONICET)
- Samuel Mimram (LIX, École Polytechnique), co-chair
- Camilo Rocha (Pontificia Universidad Javeriana), co-chair
- Femke van Raamsdonk (VU University Amsterdam)
- Sarah Winkler (University of Bolzano)
IWC Steering Committee
- 1st IWC, Nagoya, 2012
- 2nd IWC, Eindhoven, 2013
- 3rd IWC, Vienna, 2014
- 4th IWC, Berlin, 2015
- 5th IWC, Obergurgl, 2016
- 6th IWC, Oxford, 2017
- 7th IWC, Oxford, 2018
- 8th IWC, Dortmund, 2019
- 9th IWC, Paris, 2020
ContactSamuel Mimram: samuel.mimram(at)lix.polytechnique.fr
Camilo Rocha: camilo.rocha(at)javerianacali.edu.co