Nominal syntax with atom substitutions

DOI10.1016/J.JCSS.2021.01.002MaRDI QIDQ2662669zbMATH OpenOpenAlexFDO

Authors Jesús Emilio Domínguez, Maribel Fernández

Publication date 14 April 2021

Published in Journal of Computer and System Sciences (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.jcss.2021.01.002

zbMATH Keywords

matchingnominal syntaxnon-capturing substitutionrewritingunification

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Recommendations

• Nominal syntax with atom substitutions: matching, unification, rewriting
• Nominal unification with atom-variables
• Dependent types for nominal terms with atom substitutions
• Nominal unification with atom and context variables
• scientific article; zbMATH DE number 2048509
• Nominal rewriting
• Nominalizing quantifiers
• scientific article; zbMATH DE number 3852452
• scientific article; zbMATH DE number 569747
• Nominal substitution at work with the global and converse modalities

Cites work

• (Nominal) unification by recursive descent with triangular substitutions
• A new approach to abstract syntax with variable binding
• A polynomial nominal unification algorithm
• An efficient nominal unification algorithm
• Automata, Languages and Programming
• Capture-avoiding substitution as a nominal algebra
• Checking overlaps of nominal rewriting rules
• Computer Science Logic
• Confluence of orthogonal nominal rewriting systems revisited
• Decidability of fourth-order matching
• Dependent types for nominal terms with atom substitutions
• FreshML: programming with binders made simple
• From nominal to higher-order rewriting and back again
• Hierarchical nominal terms and their theory of rewriting
• scientific article; zbMATH DE number 1612495 (Why is no real title available?)
• scientific article; zbMATH DE number 176135 (Why is no real title available?)
• scientific article; zbMATH DE number 1142316 (Why is no real title available?)
• scientific article; zbMATH DE number 3336816 (Why is no real title available?)
• Logic Programming
• Nominal (universal) algebra: equational logic with names and binding
• Nominal equational logic
• Nominal logic, a first order theory of names and binding
• Nominal Matching and Alpha-Equivalence
• Nominal rewriting
• Nominal syntax with atom substitutions: matching, unification, rewriting
• Nominal unification
• On the undecidability of second-order unification
• Permissive nominal terms and their unification: an infinite, co-infinite approach to nominal techniques
• The First-Order Nominal Link
• The undecidability of the second-order unification problem
• Third order matching is decidable
• Unifying nominal unification
• α lean TA P: A Declarative Theorem Prover for First-Order Classical Logic

Cited in

(1)

• Nominal syntax with atom substitutions: matching, unification, rewriting

Describes a project that uses

Uses Software

• aleanTAP
• FreshML

This page was built for publication: Nominal syntax with atom substitutions

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