# Nominal C-Unification

arXiv: https://arxiv.org/abs/1709.05384 · HTML: https://mlsanity.com/paper/1709.05384/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 15 Sep 2017.

## Built on by (most cited first, 1 of 1)

- [Nominal Unification and Matching of Higher Order Expressions with Recursive Let](https://mlsanity.com/paper/2102.08146/) (2021)

## Abstract (arXiv)

Nominal unification is an extension of first-order unification that takes into account the α-equivalence relation generated by binding operators, following the nominal approach. We propose a sound and complete procedure for nominal unification with commutative operators, or nominal C-unification for short, which has been formalised in Coq. The procedure transforms nominal C-unification problems into simpler (finite families) of fixpoint problems, whose solutions can be generated by algebraic techniques on combinatorics of permutations.