Abstract
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 their complexity.
Author supplied keywords
Cite
CITATION STYLE
APA
Schmidt-Schauß, M., Kutsia, T., Levy, J., & Villaret, M. (2017). Nominal unification of higher order expressions with recursive let. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 10184 LNCS, pp. 328–344). Springer Verlag. https://doi.org/10.1007/978-3-319-63139-4_19
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
Already have an account? Sign in
Sign up for free