International Workshop on Unification

FSCD 2017 Workshop
September 3rd, 2017

Department of Computer Science (Oxford e-Research Centre)

OERC Building, 7 Keble Road, OX1 3QC

Enter the building from main entrance in KEBLE RD.


The UNIF informal dinner will be at

The Red Lion, 14 Gloucester St, Oxford OX1 2BN

The schedule is available! (with links to the final papers)

We're organizing an informal dinner after the workshop. Let is know at if you'd like to join :)


UNIF 2017 will be the 31th 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. 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

Invited Speakers

  • Jesper Cockx (KU Leven)
  • Ashish Tiwari (SRI International)


9.00 Registration & coffee
9.30 Ashish Tiwari — One context unification: What we know (invited talk)
One context unification extends first-order unification by introducing a single context variable, possibly with multiple occurrences. One context unification is known to be in NP, but it is not known to be solvable in polynomial time. In this talk, we motivate the context unification problem through its application in inter-procedural program analysis. We then present an NP procedure for the problem, followed by a polynomial time algorithm for certain interesting classes of the one context unification problem. The fascinating thing about one context unification is that it is very close to first-order unification and our algorithm itself is presented as an inference system that extends the usual inference rules for first-order unification. The algorithm is of independent value as it can be used, with slight modifications, to solve other problems, such as the first-order unification problem that tolerates one clash.
10.30 Pavlos Marantidis, Franz Baader — Language equations for approximate matching in the Description Logic FL0   [PDF]
Matching is the special case of unification where one of the sides to be unified has no variables and thus remains unchanged under substitutions. In Description Logics (DLs), matching concepts against patterns (concepts with variables) was introduced to help filter out unimportant aspects of complicated concepts appearing in large industrial knowledge bases. Unification of patterns was suggested as a means to detect redundancies in ontologies, by finding different concepts that may potentially stand for the same intuitive notion. Recently, approximate unification was introduced in order to increase the recall of classical unification, i.e., find substitutions that are “almost” unifiers rather than exact unifiers. In the DL FL0, the problem can be reduced to approximately solving formal language equations. Adapting a similar technique, we investigate the language equations obtained from approximate matching in FL0 and provide algorithms to approximately solve said equations.
11.00 Coffee Break
11.30 Jesus Dominguez, Maribel Fernandez — Undecidability of Nominal Unification with Atom Substitutions   [PDF]
We consider a syntax for nominal terms extended with non-capturing atom substitution and show that unification over such terms is undecidable. The proof of undecidability is obtained by reducing Hilbert's tenth problem to unification of extended nominal terms, adapting Goldfarb's proof of undecidability of second-order unification.
12.00 Yunus David Kerem Kutz, Manfred Schmidt-Schauss — Most General Unifiers in Generalized Nominal Unification   [PDF]
We consider the generalisation of nominal unification where besides expression variables, also atom variables are considered. It is known that in both cases most general unifiers exist for a solvable input constraint. A most general unifier consists of a substitution and a set of freshness constraints, where the latter is an implicit restriction on the instances of the substitution. In the general case with atom variables, we focus in this paper on an improved computation of the most general unifier, and show that a general unifier can be computed in quadratic time. Applications of this algorithm are in reasoning about program transformations in higher order functional languages.
12.30 David Sabel —Matching of Meta-Expressions with Recursive Bindings   [PDF]
We describe a matching algorithm to solve the so-called letrec matching problem. The meta-expressions occurring in the matching equations stem from a meta-language that uses higher-order abstract syntax augmented by meta-notation for recursive let, contexts, sets of bindings, and chain variables. Additionally, three kinds of constraints can be added to meta-expressions to express usual constraints on evaluation rules and program transformations. We provide a sound and complete matching algorithm ithat it runs in non-deterministic polynomial time. We show that the letrec matching problem is NP-complete.
13.00 Lunch Break
14.00 Jesper Cockx — Depending on equations: a proof-relevant framework for unification in dependent type theory (invited talk)
Typecheckers for dependently typed languages such as Agda, Idris, or Coq use unification to check definitions by dependent pattern matching. Though dependent type theory is a rich theory with higher-order terms, the unification algorithm used is typically a simple first-order one. There are however some considerations unique to the setting of dependent types:
- To see whether a unification rule can be applied, it is essential to know the type of an equation as well as its left- and right-hand sides.
- The left- and right-hand side of an equation can have different types, that only become equal after the preceding equations have been solved.
- Dependently typed languages have their own internal notion of equality (in the form of the identity type), which has to be respected by the unification algorithm. This is especially important for new type theories such as homotopy type theory (HoTT) that add certain extra structure to the identity type.
In this talk, I will present our framework for unification in a dependently typed setting. This framework treats unification problems and unification rules as internal to the type theory, rather than belonging to some external tool. Firstly, we represent a unification problem as a telescopic equation: a list of (typed) equations where the type of each equation can depend on the solution to previous equations. This allows us to keep track of dependencies between the equations precisely, and introduce new unification rules that exploit the dependencies between the equations. Secondly, a unification algorithm in our framework produces not just a substitution but also evidence that the given equations are satisfied under this substitution. This evidence guarantees that all unification rules respect the type theory's notion of equality. Finally, we give a novel characterization of a most general unifier as a (type theoretic) equivalence between the original telescope of equations and the trivial one. This gives us not only a very elegant way to define most general unifiers, but it also turns out to be useful for the compilation of functions defined by dependent pattern matching.
15.00 Makoto Hamana — Functional Implementation of Function-as-Constructor Unification   [PDF]
It is widely known that Miller's higher-order patterns provide a decidable class of higher-order unification. These have been used as the basic term structure for pattern matching in various computational systems, such as higher-order logic programming and higher-order rule based computation. However, the class of higher-order patterns is a bit restrictive in practice. Recently, Libal and Miller present a new decidable class of higher-order unification problems called Functions-as-Constructors unification (FCU). It extends the class of higher-order patterns and retains good properties of pattern unification, namely, it ensures the existence of the most general unifier. In this abstract, we report that FCU unification can be implemented functionally as an extension of Nipkow's functional pattern unification. We have implemented the FCU unification in Haskell, which has been a part of our SOL system for critical pair checking of higher-order rules.
15.30 Coffee Break
16.00 Catherine Meadows — Some Unification Problems Arising From Symbolic Cryptography   [PDF]
Unification theory has found significant applications in cryptographic protocol analysis, but that is not the only security area in which it can be applied. Here we discuss recent research in the automatic generation and verification of cryptographic algorithms, and show how it can be used to find attacks on modes of encryption. We describe an algorithm we have recently developed based on the Baader-Schulz combination procedure, and we discuss some open research problems.
16.30 Veena Ravishanka, Kimberly Gero, Paliath Narendran — Asymmetric Unification and Disunification  [PDF]
We compare two kinds of unification problems: Asymmetric Unification and Disunification, which are variants of Equational Unification. Asymmetric Unification is a type of Equational Unification where the right‑hand sides of the equations are in normal form with respect to the given term rewriting system. In Disunification we solve equations and disequations with respect to an equational theory. We contrast the time complexities of both and show that the two problems are incomparable: there are theories where one can be solved in polynomial time while the other is NPhard. This goes both ways. The time complexity also varies based on the termination ordering used in the term rewriting system.
17.00 Serdar Erbatur, Andrew M. Marshall, Christophe Ringeissen — Non-Disjoint Combination with Forward-Closed Theories  [PDF]
We investigate the unification problem in equational theories involving convergent forward-closed term rewrite systems. In the class of forward-closed theories, unification is decidable and finitary. Furthermore, forward-closed theories are syntactic theories admitting\ a terminating mutation-based unification procedure. We first demonstrate this result by showing that a mutation-based unification algorithm, originally developed for equational theories saturated by paramodulation, remains sound and complete for forward-closed theories. Building on this result we use the new mutation-based algorithm to develop an algorithm that solves the unification problem in unions of forward-closed theories with non-disjoint theories. The resulting algorithm can be viewed as a terminating instance of a procedure initiated for hierarchical combination.
17.30 Zümrüt Akçam, Daniel S. Hono Ii, Paliath Narendran —On Problems Dual to Unification   [PDF]
In this paper, we investigate a problem dual to the unification problem, namely the Common Term (CT) problem for string rewriting systems. Our main motivation was in computing fixed points in systems, such as loop invariants in programming languages. We show that the fixed point problem is reducible to the common term problem. We also prove that the common term problem is undecidable for dwindling string rewriting systems.
18.00 Wrap Up

Accepted Papers

Yunus David Kerem Kutz, Manfred Schmidt-Schauss
Most General Unifiers in Generalized Nominal Unification
Zümrüt Akçam, Daniel S. Hono Ii, Paliath Narendran
On Problems Dual to Unification
Veena Ravishanka, Kimberly Gero, Paliath Narendran
Asymmetric Unification and Disunification
Serdar Erbatur, Andrew M. Marshall, Christophe Ringeissen
Non-Disjoint Combination with Forward-Closed Theories

Call For Papers & Important Dates

Download Full CFP Submit Your Paper

Paper submission: June 21st (11pm59 CET) (Deadline extended: June 26th (11pm59 CET))
Notification of acceptance: July 21st
Workshop: September 3rd

We invite submissions of abstracts (5) pages in easychair style. 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 homepage: UNIF homepage. Based on the number and quality of submissions we will decide whether to organize a special journal issue.

Submissions in the form of extended abstracts must be at most 5 pages long.

At least one author of each accepted abstract is expected to represent it at the workshop.



  • Adrià Gascón (Edinburgh)
  • Christopher Lynch (Clarkson)

Program Committee

  • Franz Baader (TU Dresden)
  • Iliano Cervesato (CMU)
  • Santiago Escobar (TU Valencia)
  • Maribel Fernández (KCL)
  • Silvio Ghilardi (Università degli Studi di Milano)
  • Artur Jeż (University of Wrocław)
  • Konstantin Korovin (Manchester University)
  • Temur Kutsia (Johannes Kepler University Linz)
  • Jordi Levy (IIIA - CSIC)
  • Andrew Marshall (University of Mary Washington)
  • Catherine Meadows (NRL)
  • Barbara Morawska (TU Dresden)
  • Paliath Narendran (University at Albany-SUNY)
  • Jan Otop (University of Wrocław)
  • Christophe Ringeissen (LORIA-INRIA)
  • Manfred Schmidt-Schauss (Goethe-University Frankfurt)
  • Mateu Villaret (Universitat de Girona)