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

(13)

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

Describes a project that uses

Uses Software

• Isabelle/HOL
• Nominal Isabelle

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)