A set-theoretic approach to linguistic feature structures and unification algorithms (I) by N. Curteanu, P.-G. Holban

“…The linguistic unification algorithm based on tableau-subsumption is outlined. …”
Get full text

A set-theoretic approach to linguistic feature structures and unification algorithms (II) by N.Curteanu, P.-G.Holban

“…The linguistic unification algorithm based on tableau-subsumption is outlined. …”
Get full text

A Machine Checked Model of Idempotent MGU Axioms For Lists of Equational Constraints by Sunil Kothari, James Caldwell

“…We present formalized proofs verifying that the first-order unification algorithm defined over lists of satisfiable constraints generates a most general unifier (MGU), which also happens to be idempotent. …”
Get full text

Towards Correctness of Program Transformations Through Unification and Critical Pair Computation by Manfred Schmidt-Schauß, Conrad Rau

“…We explore cases where the computation of these overlaps can be done in a first order way by variants of critical pair computation that use unification algorithms. As a case study we apply the method to a lambda calculus with recursive let-expressions and describe an effective unification algorithm to determine all overlaps of a set of transformations with all reduction rules. …”
Get full text

Constraint solving in non-permutative nominal abstract syntax by Matthew R. Lakin

“…The most commonly used constraint solving algorithm over nominal abstract syntax is the Urban-Pitts-Gabbay nominal unification algorithm, which is well-behaved, has a well-developed theory and is applicable in many cases. …”
Get full text

Unification of Higher-order Patterns modulo Simple Syntactic Equational Theories by Alexandre Boudet

“…The algorithm by Miller [17] for pattern unification, refined by Nipkow [18] is first modified in order to behave as a first-order unification algorithm. Then the mutation rule for syntactic theories of Kirchner [13,14] is adapted to pattern E-unification. …”
Get full text

On Unification Modulo One-Sided Distributivity: Algorithms, Variants and Asymmetry by Andrew M Marshall, Catherine Meadows, Paliath Narendran

“…We give the first asymmetric unification algorithm for one-sided distributivity.…”
Get full text

On Nominal Syntax and Permutation Fixed Points by Mauricio Ayala-Rincón, Maribel Fernández, Daniele Nantes-Sobrinho

“…Based on this notion of equivalence, we show that C-unification is finitary and we provide a sound and complete C-unification algorithm, as a first step towards the development of nominal unification modulo AC and other equational theories with permutative properties.…”
Get full text

Type inference and strong static type checking for Promela by Donaldson, A, Gay, S

“…To handle subtyping between base types, we present an extension to a standard unification algorithm to solve a system of equality and subtyping constraints, based on bounded substitutions.…”

Parallel algorithms for free and associative-commutative unification by Hains, G

“…The use of compact terms greatly simplifies free term matching and gives rise to a linear-time algorithm with lower processing overheads than the Paterson-Wegman unification algorithm. A sublinear-time solution to the same problem is also given, assuming preloaded data. …”

Revisiting Graph Types in HyperLMNtal: A Modeling Language for Hypergraph Rewriting by Alimujiang Yasen, Kazunori Ueda

“…However, the concept of graph types for hypergraphs has not been studied in sufficient detail, and our recent work revealed that the encoding of a unification algorithm modulo <inline-formula> <tex-math notation="LaTeX">$\alpha $ </tex-math></inline-formula>-equivalence requires further evolution of graph types. …”
Get full text

A Bi-Directional Refinement Algorithm for the Calculus of (Co)Inductive Constructions by Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen, Enrico Tassi

“…Moreover, thanks to bi-directionality, the coercion system for sub-typing is more effective and type inference generates simpler unification problems that are more likely to be solved by the inherently incomplete higher order unification algorithms implemented. Finally we introduce in the external syntax the notion of vector of placeholders that enables to omit at once an arbitrary number of arguments. …”
Get full text