Nominal Unification of Higher Order Expressions with Recursive Let
Not on the map. Why?
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.
Key facts. Cited by 1 paper in the map (data through 14 Oct 2026). First posted on arXiv 12 Aug 2016.
Builds on
No reference list yet.
Built on by
Citing papers per year: 2021: 1.
1 paper.