FSCD 2017 Workshop
September 3rd, 2017
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 nonexhaustive list of topics of interest includes:
9.00  Registration & coffee 
9.30  Ashish Tiwari — One context unification: What we know (invited talk) 
One context unification extends firstorder 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 interprocedural 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 firstorder
unification and our algorithm itself is presented as an inference
system that extends the usual inference rules for firstorder
unification. The algorithm is of independent value as it can be used,
with slight modifications, to solve other problems, such as the
firstorder 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 noncapturing 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 secondorder unification.


12.00  Yunus David Kerem Kutz, Manfred SchmidtSchauss — 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 MetaExpressions with Recursive Bindings [PDF] 
We describe a matching algorithm to solve the socalled letrec matching problem.
The metaexpressions occurring in the matching equations stem from a metalanguage that uses higherorder abstract syntax augmented by metanotation for recursive let, contexts, sets of bindings, and chain variables. Additionally, three kinds of constraints can be added to metaexpressions to express usual constraints on evaluation rules and program transformations.
We provide a sound and complete matching algorithm ithat it runs in nondeterministic polynomial time. We show that the letrec matching problem is NPcomplete.


13.00  Lunch Break 
14.00  Jesper Cockx — Depending on equations: a proofrelevant 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 higherorder terms, the unification algorithm used is typically a simple firstorder 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 righthand sides.  The left and righthand 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 FunctionasConstructor Unification [PDF] 
It is widely known that Miller's higherorder patterns provide a
decidable class of higherorder unification. These have been used as the
basic term structure for pattern matching in various computational
systems, such as higherorder logic programming and higherorder rule
based computation. However, the class of higherorder patterns is a bit
restrictive in practice.
Recently, Libal and Miller present a new decidable class of higherorder
unification problems called FunctionsasConstructors unification (FCU).
It extends the class of higherorder 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 higherorder 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 BaaderSchulz 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.


TBD


17.00  Serdar Erbatur, Andrew M. Marshall, Christophe Ringeissen — NonDisjoint Combination with ForwardClosed Theories [PDF] 
We investigate the unification problem in equational
theories involving convergent forwardclosed term rewrite systems. In
the class of forwardclosed theories, unification is decidable and
finitary. Furthermore, forwardclosed theories are syntactic theories
admitting\ a terminating mutationbased unification procedure. We
first demonstrate this result by showing that a mutationbased
unification algorithm, originally developed for equational theories
saturated by paramodulation, remains sound and complete for
forwardclosed theories. Building on this result we use the new
mutationbased algorithm to develop an algorithm that solves the
unification problem in unions of forwardclosed theories with
nondisjoint theories. The resulting algorithm can be viewed as a
terminating instance of a procedure initiated for hierarchical
combination.


TBD


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