UNIF on Friday, August 11th

Session 1: Unification Modulo Theories (11:00‑12:30)

11:00‑11:30	Max Tuengerthal (University of Kiel) Ralf Kuesters (Christian-Albrechts-Universität zu Kiel) Mathieu Turuani (Loria-Inria) Implementing a Unification Algorithm for Protocol Analysis with XOR Unification algorithms are central components in constraint solving procedures for security protocol analysis. For the analysis of security protocols with XOR a unification algorithm for an equational theory including ACUN is required. While such an algorithm can easily be obtained using general combination methods such methods do not yield practical unification algorithms. In this work, we present a unification algorithm for an equational theory including ACUN which performs well in practice and is well-suited as a subprocedure in constraint solving procedures for security protocols with XOR. Our algorithm contains several optimizations which make use of the specific properties of the equational theories at hand. The efficiency of our implementation is demonstrated by experimental results.
11:30‑12:00	Pascal Lafourcade (LSV, ENS de Cachan, and LIF, Universite Marseille-1) Denis Lugiez (LIF, Universite Marseille-1) Ralf Treinen (LSV, ENS de Cachan) ACUNh: Unification and Disunification Using Automata Theory We show several results about unification problems in the equational theory ACUNh consisting of the theory of \emph{exclusive or} with one homomorphism. These results are shown using only techniques of automata and combinations of unification problems. We show how to construct a most-general unifier for ACUNh-unification problems with constants using automata. We also prove that the first-order theory of ground terms modulo ACUNh is decidable if the signature does not contain free non-constant function symbols, and that the existential fragment is decidable in the general case. Furthermore, we show a technical result about the set of most-general unifiers obtained for general unification problems.
12:00‑12:30	Paliath Narendran (University at Albany---SUNY) Pavithra Ramarathnam (University at Albany--SUNY) Unification modulo ACUI with collapsing homomorphisms We consider several equational unification problems that involve an associative-commutative operator and one or two homomorphisms. When there are two homomorphisms, one of them is assumed to be {\em collapsing,\/} i.e., $h(h(x)) = h(x)$. Complexity bounds are derived for {\em unification with constants\/} modulo these theories.

Lunch break (12:30‑14:00)

Session 2: Higher-Order Unification (14:00‑15:00)

14:00‑14:30

Sjaak Smetsers (Radboud Univerity Nijmegen) Arjen van Weelden (Radboud University Nijmegen) Bracket Abstraction Preserves Typability Bracket abstraction is an algorithm that transforms lambda expressions into combinator terms. There are several versions of this algorithm depending on the actual set of combinators that is used. Most of them have been proven correct with respect to the operational semantics. In this paper we focus on typability. We present a fully machine verified proof of the property that bracket abstraction preserves types; the types assigned to an expression before and after performing bracket abstraction are identical. To our knowledge, this is the first time that (1) such proof has been given, and (2) the proof is verified by a theorem prover. The theorem prover used in the development of the proof is PVS.

14:30‑15:00

Edwin Westbrook (Washington University in Saint Louis) Pattern Solutions to Higher-Order Unification Problems Decidable fragments of higher-order unification have been shown to be useful in many branches of computer science. One such fragment, the patterns fragment, pervades many applications of higher-order unification. In the present work we consider using the patterns fragment to restrict the solution space instead of the problem space: only solutions whose toplevel variables have rigid occurrences in their bodies are considered. We also show that this problem is decidable and in NEXPTIME for higher-order unification problems that are ordered in a specific way by a partial ordering on their unification variables. Finally an application of this problem to type inference is briefly discussed.

Session 3: Equations on Languages (15:00‑15:30)

15:00‑15:30

Franz Baader (TU Dresden) Alexander Okhotin (Rovira i Virgili University) Complexity of language equations with one-sided concatenation and all Boolean operations Language equations are equations where both the constants ocurring in the equations and the solutions are formal languages. They have first been introduced in formal language theory, but are now also considered in other areas of computer science. In particular, they can be seen as unification problems in the algebra of languages whose operations are the Boolean operations and concatenation. They are also closely related to monadic set constraints. In the present paper, we restrict the attention to language equations with one-sided concatenation, but in contrast to previous work on these equations, we allow not just union but all Boolean operations to be used when formulating them. In addition, we are not just interested in deciding solvability of such equations, but also in deciding other properties of the set of solutions, like its cardinality (finite, infinite, uncountable) and whether it contains least/greatest solutions. We show that all these decision problems are ExpTime-complete.

Break (15:30‑16:00)

Session 4: Unification with Flexible Arity Symbols (16:00‑17:00)

16:00‑16:30

Jorge Coelho (Instituto Superior de Engenharia do Porto & LIACC) Mário Florido (Univeristy of Porto DCC-FC & LIACC) Unification with Flexible Arity Symbols: a Typed Approach In this paper we extend unification of terms with flexible arity function symbols with regular expression operators such as repetition (*), alternation, etc, that are used as types allowing a compact representation of terms with functors with an arbitrary number of arguments. This new unification can then be used to unify subterms in the middle of complexes sequences of terms leading to a quite simple representation of sequences of arguments.

16:30‑17:00

Temur Kutsia (Johannes Kepler University of Linz) Mircea Marin (University of Tsukuba) Solving Regular Constraints for Hedges and Contexts We propose an algorithm for constraint solving over hedges and contexts built over individual, sequence, function, and context variables and flexible arity symbols, where the admissible bindings of sequence variables and context variables can be constrained to languages represented by regular hedge or regular context expressions. We identify sufficient syntactic restrictions that enable to solve such constraints by matching techniques, and describe a solving algorithm that is sound and complete.

Session 5: Term Rewriting Systems (17:00‑17:30)

17:00‑17:30

Adel bouhoula (École Supérieure des Télécommunications) Florent Jacquemard (INRIA & LSV) Automating Sufficient Completeness Check for Conditional and Constrained TRS We present a procedure for checking sufficient completeness for conditional and constrained term rewriting systems with axioms for constructors which may be constrained (by e.g. equalities, disequalities, ordering, membership...). Such axioms allow to specify complex data structures like e.g. sets, sorted lists or powerlists. Our approach is in- tegrated in a framework for inductive theorem proving based on tree grammars with constraints, a formalism which permits an exact repre- sentation of languages of ground constructor terms in normal form. The is based on a generalized form of narrowing where, given a term, instead of unifying it with left members of rewrite rules, we instantiate it, at selected variables, following the pro- ductions of the constrained tree grammar, and test whether it can be rewritten. It is sound and complete and has been successfully applied, yielding very natural proofs and, in case of negative answer, a counter example suggesting how to complete the specification. Moreover, it is a decision procedure when the TRS is unconditional but constrained, for a large class of constrained constructor axioms.