On nominal syntax and permutation fixed points

MaRDI QIDQ5216313zbMATH OpenFDO

Authors Mauricio Ayala-Rincón, Maribel Fernández, Daniele Nantes-Sobrinho

Publication date 17 February 2020

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

zbMATH Keywords

nominal syntaxunificationequational theoriesalpha-conversion

Mathematics Subject Classification ID

Logic in computer science (03B70) Computer science (68-XX)

Recommendations

• Fixed-point constraints for nominal equational unification
• On solving nominal fixpoint equations
• Nominal C-unification
• Nominal unification
• Permissive nominal terms and their unification: an infinite, co-infinite approach to nominal techniques

Cites work

• scientific article; zbMATH DE number 592368 (Why is no real title available?)
• A Unification Algorithm for Associative-Commutative Functions
• A formalisation of nominal \(\alpha\)-equivalence with A and AC function symbols
• A formalisation of nominal \(\alpha\)-equivalence with A, C, and AC function symbols
• A new approach to abstract syntax with variable binding
• A polynomial nominal unification algorithm
• An efficient nominal unification algorithm
• Associative-commutative unification
• Capture-avoiding substitution as a nominal algebra
• Complete axiomatizations of some quotient term algebras
• Complexity of matching problems
• Equivariant unification
• Fixed-point constraints for nominal equational unification
• Nominal logic, a first order theory of names and binding
• Nominal rewriting
• Nominal sets. Names and symmetry in computer science
• Nominal unification of higher order expressions with recursive let
• Term Rewriting and All That
• Unification in permutative equational theories is undecidable
• αCheck: A mechanized metatheory model checker

Cited in

(5)

• Unranked Nominal Unification
• Strong nominal semantics for fixed-point constraints
• Equational reasoning modulo commutativity in languages with binders
• A nominal approach to equational problems in languages with binders
• Nominal AC-matching

This page was built for publication: On nominal syntax and permutation fixed points

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