8th International Workshop on Confluence

June 28, 2019

Collocated with FSCD, June 24-30, 2019

Extended Deadline: April 22 abstract, April 29 paper

The 8th International Workshop on Confluence (IWC 2019) aims at promoting further research in confluence and related properties. Confluence provides a general notion of determinism and has always been conceived as one of the central properties of rewriting. Recently there is a renewed interest in confluence research, resulting in new techniques, tool support, certification as well as new applications. The workshop aims at promoting further research in confluence and related properties.

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, constrained rewriting, conditional rewriting, etc. Recently there is a renewed interest in confluence research, resulting in new techniques, tool supports, certification as well as new applications.

TOPICS:
Specific topics of interest include:
* confluence and related properties (unique normal forms, commutation, ground confluence)
* completion
* critical pair criteria
* decidability issues
* complexity issues
* system descriptions
* certification
* applications of confluence

The objective of this workshop is to bring together theoreticians and practitioners to promote new techniques and results, and to facilitate feedback on the implementation and application of such techniques and results in practice. IWC 2019 also aims to be a forum for presenting and discussing work in progress, and therefore to provide feedback to authors on their preliminary research.

IWC 2019 is a satellite workshop of Formal Structures for Computation and Deduction (FSCD'19) in Dortmund. Previous editions took place in Oxford (2018 and 2017), Obergurgl (2016), Berlin (2015), Vienna (2014), Eindhoven (2013) and Nagoya (2012).
More information about the workshop can be found in the home page of IWC.

Submissions

We solicit short papers or extended abstracts of at most five pages. There will be no formal reviewing. In particular, we welcome short versions of recently published articles and papers submitted elsewhere. The program committee checks relevance and may provide additional feedback. The accepted papers will be made available electronically before the workshop. The page limit for papers is 5 pages in EasyChair style. Short papers or extended abstracts must be submitted electronically through the EasyChair system at:

https://www.easychair.org/conferences/?conf=iwc2019

EasyChair style:
http://easychair.org/publications/for_authors

Important Dates

  • Title and Abstract:   April 14, 2019 Extended to April 22
  • Paper Submission:   April 21, 2019 Extended to April 29
  • Notification to authors:   May 24, 2019
  • Workshop date:   June 28, 2019

Invited Speakers

  • Cynthia Kop Radboud Universiteit Nijmegen
    Higher-order Termination
    Abstract: In the area of higher-order term rewriting, both confluence and termination are interesting -- and closely interrelated -- questions. Among the challenges in this area is the variety of similar but not quite equivalent formalisms that are considered "higher-order". In this talk, I will discuss these challenges from the viewpoint of termination, and present key termination techniques used by the tool WANDA.
  • Francisco Durán Universidad de Málaga
    On the Ground Confluence of Order-sorted Conditional Specifications Modulo Axioms: Maude's Church-Rosser Checker
    Abstract: Maude's Church-Rosser Checker (CRC) can be used to prove the ground local confluence of order-sorted conditional specifications modulo associativity/commutativity/identity axioms. It supports three complementary methods. Method 1 uses non-joinable critical pairs as completion hints to either achieve local confluence or reduce the number of critical pairs. Method 2 uses an inductive joinability inference system to try to prove the critical pairs ground joinable. Method 3 is used to prove the ground local confluence of a conditional equational specification whose conditions belong to a subspecification that has already been proved ground confluent and operationally terminating, and that is conservatively extended by the overall specification.

Programme

Joint HOR + IWC Programme
Pictures: Ph1, Ph2, P31, Ph4, Ph5,

    Session 1 Chair: Mauricio Ayala-Rincón

  • 09:00-9:15 Welcome
  • 09:15-10:00 Invited Talk: Higher-order Termination Cynthia Kop
  • 10:00-10:30 Coffe Break
    • <

    Session 2 Chair: Jakob Grue Simonsen

  • 10:30-11:00 RP IWC: Proving Non-Joinability using Weakly Monotone Algebras Bertram Felgenhauer and Johannes Waldmann
  • 11:00-11:30 RP IWC: The Diamond Lemma for non-terminating rewriting systems using deterministic reduction strategies Cyrille Chenavier and Maxime Lucas
  • 11:30-12:00 RP IWC: infChecker, a tool for checking infeasibility Raúl Gutiérrez and Salvador Lucas
  • 12:00-12:30 RP HOR: SizeChangeTool: A Termination Checker for Higher-Order Rewriting with Dependent Types Guillaume Genestier
  • 12:30-14:00 Lunch Break

    • Session 3 Chair: Silvia Ghilezan

  • 14:00-14:45 Invited Talk: Higher-Order Complexity Analysis With First-Order Tools Martin Avanzini
  • 14:45-15:30 Invited Talk: On the Ground Confluence of Order-sorted Conditional Specifications Modulo Axioms: Maude's Church-Rosser Checker Francisco Durán
  • 15:30-16:00 Coffe Break

    • Session 4 Chair: Stefano Guerrini

  • 16:00-16:45 Invited Talk: On the Clocked Lambda-Calculus Jörg Endrullis
  • 16:45-17:30 Invited Talk: Degrees of extensionality in the theory of Böhm trees Giulio Manzonetto
  • 17:30-18:00 RP IWC: Residuals Revisited Christina Kohl and Aart Middeldorp
  • 18:00-18:30 CoCo report Aart Middeldorp

Proceedings

Joint HOR 2019 and IWC 2019 Proceedings: pdf
(with system descriptions of the 8th Confluence Competition (CoCo 2019))

Committees

Program Committee

FSCD 2019 Organising Committee

  • FSCD Conference Chair: Jakob Rehof (TU Dortmund)
  • FSCD Workshops Chair: Boris Düdder (TU Dortmund)

Registration

See the FSCD 2019 Webpage

IWC 2019 Contacts

Mauricio Ayala-Rincón: ayala(at)unb.br
Jakob Grue Simonsen: simonsen(at)di.ku.dk

Support