UNIF 2016

The 30th International Workshop on Unification


The 30th International Workshop on Unification

is the 30th event in a series of international
meetings devoted to unification theory and its applications.
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.

The International Workshop on Unification (UNIF) is a yearly
forum for researchers in unification theory and related
fields to meet old and new colleagues, to present recent
(even unfinished) work, and to discuss new ideas and trends.
It is also a good opportunity for young researchers and
scientists working in related areas to get an overview of the
current state of the art in unification theory.

The workshop will be  hosted by the 1st International Conference on
Formal Structures for Computation and Deduction (FSCD, Porto, June

Registration is open:

the registration form is available here.

Description of the Topic

Unification is one of the central notions in automated reasoning and lies at the
heart of many reasoning systems. Unification is concerned with the problem of
making two terms equal, either syntactically or modulo a theory.
UNIF 2016 will be the 30th 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 at
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. A non-exhaustive list of topics
of interest includes:

  • Unification algorithms, calculi and implementations
  • Equational unification and unification modulo theories
  • Unification in modal, temporal and description logics
  • Admissibility of Inference Rules
  • Narrowing
  • Matching algorithms
  • Constraint solving
  • Combination problems
  • Disunification
  • Higher-Order Unification
  • Type checking and reconstruction
  • Typed unification
  • Complexity issues
  • Query answering
  • Implementation techniques
  • Applications of unification
  • Antiunification/Generalization

Submission Details

Following the tradition of UNIF, we call for submissions of
abstracts (5 pages) in EasyChair style, to be submitted
electronically as PDF files through the EasyChair submission


Abstracts will be evaluated by the Programme Committee
(if necessary with support from external reviewers)
regarding their significance for the workshop. Accepted
abstracts will be presented at the workshop and included in
the informal proceedings of the workshop, available in printed
form at the workshop and in electronic form from the UNIF


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