Welcome to UNIF 2018 in Oxford

UNIF 2018 will be the 32nd 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.

UNIF 2018 is affiliated with the Third International Conference on Formal Structures for Computation and Deduction FSCD 2018, part of the Federated Logic Conference 2018 () in Oxford.

Call for Papers

The International Workshop on Unification 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 state of the art in unification theory. UNIF welcomes submissions describing research on all aspects of unification and its applications. Suggested topics include but are not limited to the following:

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 Formalisation of unification
Applications of unification

Submission instructions

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 site:


Abstracts will be evaluated by the Programme Committee (if necessary with support from external reviewers) regarding their significance for the workshop. We will allow work presented/submitted in/to another conference.

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 homepage.

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

Important Dates

  • Submission of title and abstracts: Monday, April 9, 2018
  • Submission of full paper: Monday, April 16, 2018
  • Author notification: Tuesday, May 15, 2018
  • Camera-ready papers: Monday, May 28, 2018
  • UNIF 2018: Saturday, July 7, 2018
  • FSCD 2018: July 9-12, 2018
  • Main conference (FLoCS): July 6-19, 2018

Invited Speakers

Silvio Ghilardi (Università degli Studi di Milano)
"Handling substitutions via duality"
Abstract: Many interesting problems concerning intuitionistic and intermediate propositional logics are related to properties of substitutions: among them, besides unification, we have rule admissibility, characterization of projective formulae, definability of maximum and minimum fixpoints, finite periodicity theorems, etc. Since all these questions can be stated in purely category-theoretic terms, they are all sensible to an approach via duality techniques. The available duality for finitely presented Heyting algebras involves both sheaves (giving the appropriate geometric framework) and bounded bisimulations (handling the combinatorics of definability aspects): we show how to use such duality to attack and solve the above problems in a uniform way.
[Recent and new results come from joint and ongoing work with Luigi Santocanale]

Adrià Gascón (The Alan Turing Institute / University of Warwick)
Title TBA
Abstract: TBA


PC Chairs

  • Mauricio Ayala-Rincón (Universidade de Brasília)
  • Philippe Balbiani (CNRS - Toulouse University)
  • Program Committee

  • Maria Alpuente (UP Valencia)
  • Franz Baader (TU Dresden)
  • Eduardo Bonelli (UN Quilmes)
  • Iliano Cervesato (Carnegie Mellon U)
  • Wojciech Dzik (U Silesia)
  • Santiago Escobar (UP Valencia)
  • Maribel Fernández (King's College London)
  • Çigdem Gencer (Istanbul Aydin U)
  • Rosalie Iemhoff (U Utrecht)
  • Emil Jeřábek (Czech Academy of Sciences)
  • Temur Kutsia (Johannes Kepler U Linz)
  • Jordi Levy (IIIA-CSIC)
  • Christopher Lynch (Clarkson U)
  • Catherine Meadows (US Naval Research Laboratory)
  • Paliath Narendran (U at Albany - State U of New York)
  • Christophe Ringeissen (Inria Nancy)
  • Manfred Schmidt-Schauß (Johann Wolfgang Goethe U Frankfurt)
  • UNIF Steering Committee

  • Barbara Morawska, Technische Universität Dresden
  • Konstantin Korovin, University of Manchester
  • Christophe Ringeissen, Inria Nancy
  • Temur Kutsia, RISC Johannes Kepler Universität Linz
  • Mateu Villaret, Universitat de Girona
  • Santiago Escobar, Universitat Politècnica de València
  • Silvio Ghilardi, Università degli Studi di Milano
  • Manfred Schmidt-Schauß, Goethe Universität Frankfurt am Main