Nominal unification with atom-variables

DOI10.1016/j.jsc.2018.04.003zbMath1395.68096MaRDI QIDQ1640638

Yunus D. K. Kutz, David Sabel, Manfred Schmidt-Schauss

Publication date: 14 June 2018

Published in: Journal of Symbolic Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.jsc.2018.04.003

zbMATH Keywords

functional languages; correctness; program transformations; nominal unification; atom-variables

Mathematics Subject Classification ID

68Q25: Analysis of algorithms and problem complexity

68Q42: Grammars and rewriting systems

68Q17: Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.)

68N30: Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)

Related Items

Unnamed Item, Nominal Unification and Matching of Higher Order Expressions with Recursive Let, Rewriting with generalized nominal unification, Ground confluence and strong commutation modulo alpha-equivalence in nominal rewriting, Confluence and commutation for nominal rewriting systems with atom-variables, Nominal unification with letrec and environment-variables

Uses Software

• Isabelle/HOL
• Nominal Isabelle

Cites Work

• Equivariant unification
• A polynomial nominal unification algorithm
• Isabelle/HOL. A proof assistant for higher-order logic
• Checking overlaps of nominal rewriting rules
• Nominal unification of higher order expressions with recursive let
• Nominal Sets
• Unifying Nominal Unification
• Constraint solving in non-permutative nominal abstract syntax
• Safety of Nöcker's strictness analysis
• An Efficient Unification Algorithm
• Computer Science Logic
• An Efficient Nominal Unification Algorithm
• The complexity of satisfiability problems
• Automata, Languages and Programming
• General Bindings and Alpha-Equivalence in Nominal Isabelle
• Nominal Unification from a Higher-Order Perspective