Nominal unification of higher order expressions with recursive let

DOI10.1007/978-3-319-63139-4_19zbMath1485.68074arXiv1608.03771OpenAlexW2511722588MaRDI QIDQ2409747

Jordi Levy, Manfred Schmidt-Schauss, Mateu Villaret, Temur Kutsia

Publication date: 13 October 2017

Full work available at URL: https://arxiv.org/abs/1608.03771

zbMATH Keywords

operational semanticslambda calculusnominal unificationhigher-order expressionsrecursive let

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Functional programming and lambda calculus (68N18) Semantics in the theory of computing (68Q55) Grammars and rewriting systems (68Q42) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (11)

Nominal unification with atom-variables ⋮ Unnamed Item ⋮ Nominal Unification and Matching of Higher Order Expressions with Recursive Let ⋮ A Certified Functional Nominal C-Unification Algorithm ⋮ Unnamed Item ⋮ Nominal AC-matching ⋮ A formalisation of nominal \(\alpha\)-equivalence with A, C, and AC function symbols ⋮ Fixed-Point Constraints for Nominal Equational Unification ⋮ A formalisation of nominal C-matching through unification with protected variables ⋮ Formalising nominal C-unification generalised with protected variables ⋮ Nominal unification with letrec and environment-variables

This page was built for publication: Nominal unification of higher order expressions with recursive let