E-Unification for Second-Order Abstract Syntax
An E-unification procedure for second-order abstract syntax: given an equational theory induced by an evaluation relation, we derive a higher-order unification procedure that operates uniformly on terms generated from any bifunctor.
This paper underpins the free-foil framework.
Kudasov, N. (2023). "E-Unification for Second-Order Abstract Syntax." In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023), LIPIcs vol. 260, pp. 10:1–10:22. DOI: 10.4230/LIPIcs.FSCD.2023.10.