IWC 2013
2nd International Workshop on Confluence

June 28, 2013, Eindhoven, The Netherlands

News

Background

Recently there is a renewed interest in confluence research, resulting in new techniques, tool support as well as new applications. The workshop aims at promoting further research in confluence and related properties. The workshop is collocated with RDP 2013. During the workshop the 2nd Confluence Competition (CoCo 2013) takes place. Previous IWC was held in Nagoya (2012).

Topics

The workshop solicits short papers/extended abstracts on the following topics:

Invited Speakers

Proceedings

PDF

Program

09:00-09:05
opening

09:05-10:00
Three Termination Problems    (invited talk)    printable pdf
Patrick Dehornoy (University of Caen)

We shall describe three termination problems originating from various areas of algebra. These are the termination of handle reduction in braid theory, where termination is proved but with a very coarse complexity bound, the termination of the Polish algorithm in the theory of self-distributive systems, where termination is not yet proved, and the termination of subword reversing in semigroup theory, where termination is proved in some cases. In all three situations, the results known so far rely on the specific properties of the underlying objects, and it would be highly desirable to know whether general techniques might help.

10:00-10:30
break

10:30-10:50
Disproving Confluence of Term Rewriting Systems by Interpretation and Ordering
Takahito Aoto
10:50-11:10
Automatically Finding Non-confluent Examples in Term Rewriting
Hans Zantema
11:10-11:30
Confluent Unfolding in the Lambda-Calculus with letrec
Jan Rochel and Clemens Grabmayer
11:30-11:50
Rule Labeling for Confluence of Left-Linear Term Rewrite Systems
Bertram Felgenhauer
11:50-12:10
Commutation via Relative Termination
Nao Hirokawa and Aart Middeldorp

12:10-14:00
lunch

14:00-14:45
Confluence and Infinity - a kaleidoscopic view    (joint invited talk with WIR 2013)
Jan Willem Klop (VU University Amsterdam and CWI Amsterdam)

In this talk we will attempt to present some highlights in old and new studies concerning the pivotal notion of confluence in lambda calculus, term rewriting and infinitary rewriting. We first aim the kaleidoscope on the classics: lambda calculus (Tait-Martin-Löf, Aczel, superdevelopments, Parallel Moves Lemma), combinatory logic and other orthogonal systems, deviating from that ideal setting by looking briefly at non-left-linear rules, such as Surjective Pairing (De Vrijer), confluence for braids, and confluence by completion (Zantema, van Oostrom)

In a second part, we rotate the kaleidoscope and view some basic confluence methods, Newman's Lemma, De Bruijn's Weak Diamond Property, Van Oostrom's Decreasing Diagrams.

In a third twist of the kaleidoscope we invoke the setting of infinitary rewriting, for orthogonal rewriting, and also for lambda calculus. We briefly show a recent remarkable coinductive setup of infinitary rewriting, and then return to infinitary confluence, signalling some striking differences with the finitary rewriting world, with as motto: confluence lost, confluence regained. We describe the Threefold Path to regain confluence, via the semantics of Böhm Trees and its two variants. Speaking about Böhm trees, we (might) turn to a more refined notion, clocked Böhm Trees, a recent method to discriminate lambda terms with respect to finitary convertibility, very suitable for fixed point combinators.

Somewhere in between we (might) show that the eta-rule wreaks havoc in infinitary lambda calculus. We conclude with the miracle of infinitary confluence for lambda-beta-Omega calculus.

15:00-15:30
2nd Confluence Competition (CoCo 2013)
chair: Harald Zankl

15:30-16:00
break

16:00-16:20
Proving Confluence of Conditional Term Rewriting Systems via Unravelings
Karl Gmeiner, Naoki Nishida and Bernhard Gramlich
16:20-16:40
A Confluent Pattern Calculus with Hedge Variables
Sandra Alves, Besik Dundua, Mário Florido and Temur Kutsia
16:40-17:00
Synchronizing Applications of the Parallel Moves Lemma to Formalize Confluence of Orthogonal TRSs in PVS
Ana Cristina Rocha Oliveira, André Luiz Galdino and Mauricio Ayala-Rincón
17:00-17:20
KBCV 2.0 - Automatic Completion Experiments
Thomas Sternagel
17:20-17:40
Confluent Let-Floating
Clemens Grabmayer and Jan Rochel

17:40-17:45
closing

Important Dates

submission April 25, 2013   (extended)
notification May 10, 2013
final version June 3, 2013
workshop June 28, 2013

Submission (closed)

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. In addition, we plan to distribute a printed version of the proceedings at 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/account/signin.cgi?conf=iwc2013

Organizing Committee

Program Committee