Constraint solving in non-permutative nominal abstract syntax

Matthew R. Lakin

Nominal abstract syntax is a popular first-order technique for encoding, and reasoning about, abstract syntax involving binders. Many of its applications involve constraint solving…