Nominal unification with atom-variables

DOI10.1016/J.JSC.2018.04.003MaRDI QIDQ1640638zbMATH OpenOpenAlexWikidataFDO

Authors David Sabel, Yunus D. K. Kutz, Manfred Schmidt-Schauß

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

program transformationscorrectnessfunctional languagesnominal unificationatom-variables

Mathematics Subject Classification ID

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

Recommendations

• Nominal unification with atom and context variables
• Unifying nominal unification
• Nominal syntax with atom substitutions: matching, unification, rewriting
• Computer Science Logic
• Nominal unification
• Nominal C-unification
• Rewriting with generalized nominal unification
• Unranked Nominal Unification

Cites work

• A polynomial nominal unification algorithm
• An Efficient Unification Algorithm
• An efficient nominal unification algorithm
• Automata, Languages and Programming
• Checking overlaps of nominal rewriting rules
• Computer Science Logic
• Constraint solving in non-permutative nominal abstract syntax
• Equivariant unification
• General bindings and alpha-equivalence in Nominal Isabelle
• Isabelle/HOL. A proof assistant for higher-order logic
• Nominal sets. Names and symmetry in computer science
• Nominal unification of higher order expressions with recursive let
• Safety of Nöcker's strictness analysis
• The complexity of satisfiability problems
• Unifying nominal unification

Cited in

(14)

• Meta-variables as infinite lists in nominal terms unification and rewriting
• Rewriting with generalized nominal unification
• Nominal unification with letrec and environment-variables
• Confluence and commutation for nominal rewriting systems with atom-variables
• Completeness in PVS of a nominal unification algorithm
• Nominal anti-unification
• Unranked Nominal Unification
• Nominal unification with atom and context variables
• Nominal syntax with atom substitutions
• Nominal unification of higher order expressions with recursive let
• Equational generalization problems with atom-variables
• Foundations of Software Science and Computational Structures
• Ground confluence and strong commutation modulo alpha-equivalence in nominal rewriting
• Nominal Unification and Matching of Higher Order Expressions with Recursive Let

Describes a project that uses

Uses Software

• Nominal Isabelle
• Isabelle/HOL

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1640638)