TítuloNominal Unification of Higher Order Expressions with Recursive Let
Publication TypeConference Paper
Year of Publication2017
AuthorsSchmidt-Schauß M, Kutsia T, Levy J, Villaret M
Conference NameRevised Selected Papers of the 26th International Symposium on Logic-Based Program Synthesis and Transformation, LOPSTR 2016
VolumeLNCS 10184
EditorialSpringer
Conference LocationEdinburgh, UK
Paginación328-344
ISBN Number978-3-319-63138-7
Resumen

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.

URLhttps://doi.org/10.1007/978-3-319-63139-4_19
DOI10.1007/978-3-319-63139-4_19