UNIF 2020
June 29, 2020
Paris, France
Co-located with IJCAR 2020
Due to the Covid-19 pandemic, the workshop will be held online along with online versions of IJCAR and FSCD. Please see the following for FSCD-IJCAR
UNIF 2020 - 34th International Workshop on Unification

UNIF 2020: The 34th International Workshop on Unification 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.

UNIF 2020 will be the 34th in a series of annual international workshops on unification. Previous editions have taken place mostly in Europe (Austria, Denmark, France, Germany, Ireland, Italy, Poland, UK), but also in the USA and Japan. For more details on previous UNIF workshops, please see the UNIF homepage

Unification is concerned with the problem of making two terms equal, finding solutions for equations, or making formulas equivalent. It is a fundamental process used in a number of fields of computer science, including automated reasoning, term rewriting, logic programming, natural language processing, program analysis, types, etc. Traditionally, the scope of the UNIF workshops has covered the topic of unification in a broad sense, encompassing also research in constraint solving, admissibility of inference rules, and applications such as type checking, query answering and cryptographic protocol analysis.

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.

Topics of interest to this forum include, but are not limited to:
 

  • Unification algorithms, calculi and implementations
  • Equational unification and unification modulo theories
  • Admissibility of Inference Rules
  • Unification in modal, fuzzy, temporal and description logics
  • Anti-unification/generalization
  • Semi-unification
  • Narrowing
  • Formalisation of unification
  • Matching Problems
  • Applications
  • Unification in Special Theories
  • Higher-Order Unification
  • Combination problems
  • Contraint Solving
  • Disunification
  • Complexity Issues
  • Type Checking and reconstruction

UNIF 2020 also aims to be a forum for presenting and discussing work in progress, and therefore to provide feedback to authors on their preliminary research. More information about UNIF can be found here.

UNIF 2020 will be a satellite workshop of The International Joint Conference on Automated Reasoning (IJCAR 2020) in Paris, France.

Call for Papers

Following the tradition of UNIF, we call for submissions of abstracts (5 pages) in EasyChair style, to be submitted electronically as PDF through the EasyChair submission site:
 
    https://easychair.org/conferences/?conf=unif2020

Accepted abstracts will be presented at the workshop and included in the informal proceedings of the workshop, available in electronic form as a technical report in the RISC-Linz Report Series from the Research Institute for Symbolic Computation, Johannes Kepler University. At least one of the authors should register for the workshop. 

Based on the number and quality of submissions we will decide whether to organize a special journal issue.

Important Dates:

  • Submission of titles and abstracts: April 13, 2020 April 20, 2020
  • Submission of full paper:  April 20, 2020 April 27, 2020
  • Author notification: May 25, 2020 June 1, 2020
  • Camera-ready papers: June 8, 2020 June 15, 2020
  • UNIF 2020: June 29, 2020
Program Commitee

  • Mauricio Ayala-Rincon (Universidade de Brasilía)   
  • Franz Baader (TU Dresden)   
  • Alexander Baumgartner (University of Chile)
  • Evelyne Contejean (LRI, CNRS, Univ Paris-Sud, Orsay)
  • Daniel Dougherty (Worcester Polytechnic Institute)
  • Besik Dundua (Ivane Javakhishvili Tbilisi State University)    
  • Serdar Erbatur (University of Texas at Dallas
  • Santiago Escobar (Universitat Politècnica de València)   
  • Maribel Fernandez (King's College London)   
  • Silvio Ghilardi (Università degli Studi di Milano)
  • Pascual Julian-Iranzo (University of Castilla-La Mancha)
  • Temur Kutsia (RISC-Johannes Kepler University Linz) co-chair
  • Jordi Levy (IIIA - CSIC)   
  • Christopher Lynch (Clarkson University)   
  • Andrew M. Marshall (University of Mary Washington) co-chair
  • Barbara Morawska (Ahmedabad University)   
  • Daniele Nantes-Sobrinho (Universidade de Brasília)   
  • Paliath Narendran (University at Albany--SUNY)   
  • Veena Ravishankar (University of Mary Washington)   
  • Christophe Ringeissen (INRIA)

Invited Speakers
  • Manfred Schmidt-Schauß - Goethe-University Frankfurt AM Main

    • Topic: Nominal Algorithms: Applications and Extensions

  • Stéphanie Delaune - Univ Rennes, CNRS, IRISA

    • Topic: Rewriting in Protocol Verification

Accepted Papers and Proceedings

Proceedings:

Proceedings of The 34th International Workshop on Unification

Accepted Papers:

Philippe Balbiani, Cigdem Gencer,     Maryam Rostamigiv and Tinko Tinchev About the unification type of modal logic K+[][]false
David Cerna, Alexander Leitsch and Anela Lolic On the Unification of Term Schemata
Paliath Narendran, Saumya Arora and Yu Zhang An Improved Algorithm for Testing Whether a Special String Rewriting System is Confluent
Thomas Prokosch and François Bry Unification on the Run
Paliath Narendran, Ashley Suchy and Yu Zhang Some Results on Prefix Grammars
Alexander Baumgartner and Daniele Nantes-Sobrinho A,C and AC Nominal Anti-Unification
Daniele Nantes-Sobrinho, Deivid Vale, Mauricio Ayala-Rincón and Maribel Fernandez An Investigation into Nominal Equational Problems
Andrew M. Marshall, Catherine Meadows, Paliath Narendran, Veena Ravishankar and Brandon Rozek Algorithmic Problems in Synthesized Cryptosystems
Serdar Erbatur, Andrew M. Marshall and Christophe Ringeissen Terminating Non-Disjoint Combined Unification
Jean-Pierre Jouannaud and Fernando Orejas Unification of Drags
Temur Kutsia and Cleo Pau Proximity-Based Unification with Arity Mismatch

Program

8:55–9:00: Welcome to UNIF

Session 1: (Security and Rewriting) Chair: Temur Kutsia

  • 9:00 - 9:45 Invited Talk: Rewriting in Protocol Verification
    • Stéphanie Delaune
  • 9:45 Algorithmic Problems in Synthesized Cryptosystems
    • Andrew M. Marshall, Catherine Meadows, Paliath Narendran, Veena Ravishankar and Brandon Rozek
  • 10:10 Terminating Non-Disjoint Combined Unification
    • Serdar Erbatur, Andrew M. Marshall and Christophe Ringeissen
  • 10:35 Some Results on Prefix Grammars
    • Paliath Narendran, Ashley Suchy and Yu Zhang

11:00 - 11:30 Virtual coffee break

Session 2: (Logic and Discrete Structures) Chair: Christophe Ringeissen

  • 11:30 About the unification type of modal logic K+[][]false
    • Philippe Balbiani, Cigdem Gencer, Maryam Rostamigiv and Tinko Tinchev
  • 11:55 On the Unification of Term Schemata
    • David Cerna, Alexander Leitsch and Anela Lolic
  • 12:20 Unification of Drags
    • Jean-Pierre Jouannaud and Fernando Orejas

12:45 - 14:00 Lunch Break

Session 3: (Nominal Techniques) Chair: Andrew Marshall

  • 14:00 - 14:45 Invited Talk: Nominal Algorithms: Applications and Extensions
    • Manfred Schmidt-Schauß
  • 14:45 A,C and AC Nominal Anti-Unification
    • Alexander Baumgartner and Daniele Nantes-Sobrinho
  • 15:10 An Investigation into Nominal Equational Problems
    • Daniele Nantes-Sobrinho, Deivid Vale, Mauricio Ayala-Rincón and Maribel Fernandez

15:35 - 16:00 Virtual coffee break

Session 4: (Improvements and Generalizations) Chair: Mauricio Ayala-Rincón

  • 16:00 Proximity-Based Unification with Arity Mismatch
    • Temur Kutsia and Cleo Pau
  • 16:25 Unification on the Run
    • Thomas Prokosch and François Bry
  • 16:50 An Improved Algorithm for Testing Whether a Special String Rewriting System is Confluent
    • Paliath Narendran, Saumya Arora and Yu Zhang

Please see the following link for the prerecorded talks: Talks

Note that you will need to register for the workshop to view the talks. If you registered and didn't receive a password for the talks, please contact the PC-Chairs.

Register

Participation will be free, but a preregistration will be required to join the video meeting.

Please see the main registration page here: Registration Form