Nominal unification with atom-variables

DOI10.1016/j.jsc.2018.04.003zbMath1395.68096OpenAlexW2795931429WikidataQ130021361 ScholiaQ130021361MaRDI 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 languagescorrectnessprogram transformationsnominal unificationatom-variables

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Grammars and rewriting systems (68Q42) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (6)

Nominal Unification and Matching of Higher Order Expressions with Recursive Let ⋮ Unnamed Item ⋮ Ground confluence and strong commutation modulo alpha-equivalence in nominal rewriting ⋮ Rewriting with generalized nominal unification ⋮ 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

This page was built for publication: Nominal unification with atom-variables