# Nominal Unification of Higher Order Expressions with Recursive Let

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

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 12 Aug 2016.

## 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)

A sound and complete algorithm for nominal unification of higher-order expressions with a recursive let is described, and shown to run in non-deterministic polynomial time. We also explore specializations like nominal letrec-matching for plain expressions and for DAGs and determine the complexity of corresponding unification problems.