Nominal narrowing

DOI10.4230/LIPICS.FSCD.2016.11MaRDI QIDQ5369476zbMATH OpenFDO

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

Publication date 17 October 2017

Full work available at URL https://doi.org/10.4230/LIPICS.FSCD.2016.11

zbMATH Keywords

matchingequational theoriesnarrowingnominal unificationnominal rewriting

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Grammars and rewriting systems (68Q42) Equational classes, universal algebra in model theory (03C05)

Recommendations

• Nominal C-unification
• Nominal unification
• Computer Science Logic
• Unifying nominal unification
• The First-Order Nominal Link

Cited in

(14)

• On solving nominal disunification constraints
• A formalisation of nominal C-matching through unification with protected variables
• A formalisation of nominal \(\alpha\)-equivalence with A and AC function symbols
• Uniform Lazy Narrowing
• Nominal C-unification
• A formalisation of nominal \(\alpha\)-equivalence with A, C, and AC function symbols
• Certified first-order AC-unification and applications.
• Nominal unification with atom and context variables
• Formalising nominal C-unification generalised with protected variables
• An Iabelle/HOL formalization of narrowing and multiset narrowing for E-unifiability, reachability and infeasibility
• αCheck: A mechanized metatheory model checker
• Nominal Unification and Matching of Higher Order Expressions with Recursive Let
• A certified functional nominal C-unification algorithm
• Nominal equational rewriting and narrowing

This page was built for publication: Nominal narrowing

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