Ground confluence and strong commutation modulo alpha-equivalence in nominal rewriting

DOI10.1007/978-3-031-17715-6_17OpenAlexW4312716460MaRDI QIDQ6109479

Kentaro Kikuchi

Publication date: 28 July 2023

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-031-17715-6_17

Mathematics Subject Classification ID

Theory of computing (68Qxx)

Cites Work

• Unnamed Item
• Unnamed Item
• A new approach to abstract syntax with variable binding
• A formalised first-order confluence proof for the \(\lambda\)-calculus using one-sorted variable names.
• Nominal unification with atom-variables
• Parallel closure theorem for left-linear nominal rewriting systems
• Checking overlaps of nominal rewriting rules
• Nominal unification
• Nominal logic, a first order theory of names and binding
• Confluence and commutation for nominal rewriting systems with atom-variables
• Nominal rewriting
• Term Rewriting and All That
• Rewriting with generalized nominal unification
• Confluence of orthogonal nominal rewriting systems revisited
• On the Church-Rosser property for the direct sum of term rewriting systems
• Tree-Manipulating Systems and Church-Rosser Theorems

This page was built for publication: Ground confluence and strong commutation modulo alpha-equivalence in nominal rewriting