iwc2020.cic.unb.br Open in urlscan Pro
164.41.168.130  Public Scan

Form analysis
0 forms found in the DOM

Text Content

9th International Workshop on Confluence
30th June 2020, Paris, France

IWC 2012 IWC 2013 IWC 2014 IWC 2015 IWC 2016 IWC 2017 IWC 2018 IWC 2019 IWC 2020
IWC 2020
News Background Topics Proceedings Program Important Dates Submission Invited
Speakers Program Committee Steering Committee Previous IWCs Contact Support


IWC 2020


9TH INTERNATIONAL WORKSHOP ON CONFLUENCE


30TH JUNE 2020, PARIS, FRANCE


COLOCATED WITH FSCD AND IJCAR


NEWS

 * June 15th, 2020: added papers and schedule.
 * April 7th, 2020: IMPORTANT INFORMATION Due to current travel restrictions in
   various countries, the meeting will be held virtually this year. The
   technical details will be given in due time.
 * December 2019: Created website.


BACKGROUND

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.

IWC 2020 is part of Paris Nord Summer of LoVe 2020, a joint event on LOgic and
VErification at Université Paris 13, made of Petri Nets 2020, IJCAR 2020, FSCD
2020, and over 20 satellite events.

The 9th Confluence Competition CoCo 2020 will run live during IWC 2020.


TOPICS

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


IMPORTANT DATES

submission (abstract): Friday, April 17th, 2020 submission (paper): Wednesday,
April 22nd, 2020 notification: Friday, May 22nd, 2020 workshop: Tuesday, June
30th, 2020

(deadlines are AoE)


ACCEPTED PAPERS

The proceedings are available online and include reports on the 9th Confluence
Competition. You can also find individual papers below:

 * Vincent van Oostrom. Some symmetries of commutation diamonds
 * Kiraku Shintani and Nao Hirokawa. Parallel Closedness Revisited
 * Benjamin Dupont, Philippe Malbos and Cyrille Chenavier. Algebraic critical
   pair lemma
 * Ugo De'Liguoro and Riccardo Treglia. On the reduction of the type-free
   computational Lambda-calculus
 * Anders Miltner, Kathleen Fisher, Benjamin Pierce, David Walker and Steve
   Zdancewic. Confluence in Lens Synthesis
 * Cameron Calk. Coherent Confluence in Modal n-Kleene Algebras
 * Eelco Visser and Eduardo Amorim. Safety and Completeness of Disambiguation
   corresponds to Termination and Confluence of Reordering
 * Jean-Pierre Jouannaud and Fernando Orejas. Confluence of drag rewriting


PROGRAM

 9:00-10:00  Frédéric Blanqui: On the use of confluence in type theory modulo rewriting - Invited Talk (slides)
10:00-10:30 Vincent van Oostrom: Some symmetries of commutation diamonds (slides)
10:30-11:00 Kiraku Shintani and Nao Hirokawa: Parallel Closedness Revisited (slides)

11:30-12:00 Benjamin Dupont, Philippe Malbos and Cyrille Chenavier:
Algebraic critical pair lemma  (slides)
12:00-12:30 Ugo De'Liguoro and Riccardo Treglia: On the reduction of the type-free
            computational Lambda-calculus (slides)
12:30-13:00 Anders Miltner, Kathleen Fisher, Benjamin Pierce, David Walker and Steve Zdancewic:
            Confluence in Lens Synthesis (slides)

14:00-15:00 9th Confluence Competition - CoCo 2020 - (slides)
            Report presented by Aart Middeldorp, Kiraku Shintani, Naoki Nishida and Johannes Waldmann
15:00-15:30 Cameron Calk: Coherent Confluence in Modal n-Kleene Algebras (slides)

16:00-17:00  Margherita Zorzi: Compositional theories for embedded programming - Invited Talk  (slides)

17:00-17:30 Eelco Visser and Eduardo Amorim: Safety and Completeness of Disambiguation corresponds
            to Termination and Confluence of Reordering (slides)
17:30-18:00 Jean-Pierre Jouannaud and Fernando Orejas: Confluence of drag rewriting  (slides)
18:00-18:05 Closing and Announcement of the IWC SC by Takahito Aoto (slides)




--------------------------------------------------------------------------------

Some screen shots: sc01 sc02 sc03 sc04 sc05 sc06 sc07 sc08 sc09 sc10 sc11 sc12

Unedited Live Broadcast

--------------------------------------------------------------------------------


INVITED SPEAKERS

 * Margherita Zorzi (Università degli Studi di Verona) Compositional theories
   for embedded programming
   Abstract: Embedded programming style allows to split the syntax in two parts,
   representing respectively a host language H and a core language C embedded in
   H. This formally models several situations in which a user writes code in a
   main language and delegates some tasks to an ad hoc domain specific language.
   Moreover, as showed in recent years, a particular case of the host-core
   approach allows a flexible management of data linearity, which is
   particularly useful in non-classical computational paradigms such as quantum
   computing. The definition of a systematised type theory to capture and
   standardize common properties of embedded languages is partially unexplored.
   We present a flexible fragment of such a type theory, together with its
   semantics in terms of enriched categories. We introduce the calculus HC0 and
   we use the notion of internal language of a category to relate the language
   to the class of its models, showing the equivalence between the category of
   models and the one of theories. This provides a stronger result w.r.t.
   standard soundness and completeness since it involves not only the models but
   also morphisms between models. We observe that the definition of the
   morphisms between models highlights further advantages of the embedded
   languages and we discuss some concrete instances, extensions and
   specializations of the syntax and the semantics.
 * Frédéric Blanqui (INRIA LSV ENS Paris - Saclay/Université Saclay) "On the use
   of confluence in type theory modulo rewriting"
   Abstract: Various proof assistants advocate the use of rewriting in type
   theory, especially Dedukti. This however raises a number of problems. In this
   talk, I will present various properties of type theory modulo.


PROGRAM COMMITTEE

 * Beniamino Accattoli (INRIA & LIX, École Polytechnique)
 * Mauricio Ayala-Rincón (Universidade de Brasília), co-chair
 * Cyrille Chenavier (Centre Inria Lille)
 * Alejandro Díaz-Caro (Universidad Nacional de Quilmes & ICC/UBA-CONICET)
 * Maribel Fernández (King's College London)
 * Mario Florido (Universidade de Porto)
 * Makoto Hamana (Gunma University)
 * Philippe Malbos (Université Claude Bernard Lyon 1)
 * Samuel Mimram (LIX, École Polytechnique), co-chair
 * Camilo Rocha (Pontificia Universidad Javeriana - Cali)
 * Daniel Lima Ventura (Universidade Federal de Goiás)
 * Femke van Raamsdonk (VU University Amsterdam)
 * Johannes Waldmann (Hochschule für Technik, Wirtschaft und Kultur Leipzig)
 * Sarah Winkler (Università degli studi di Verona)


IWC STEERING COMMITTEE

 * Takahito Aoto
 * Nao Hirokawa


PREVIOUS IWCS

 * 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
 * 9th IWC, Dortmund, 2019


CONTACT

Mauricio Ayala-Rincón: ayala(at)unb.br
Samuel Mimram: samuel.mimram(at)lix.polytechnique.fr


SUPPORT