An initial algebra approach to term rewriting systems with variable binders

DOI10.1007/s10990-006-8747-5zbMath1105.68055OpenAlexW1973544374MaRDI QIDQ853743

Makoto Hamana

Publication date: 17 November 2006

Published in: Higher-Order and Symbolic Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10990-006-8747-5

zbMATH Keywords

Term rewriting systemsAbstract syntax with variable bindingHigher-order abstract syntaxInitial algebra semantics

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Related Items (2)

Size-based termination of higher-order rewriting ⋮ Termination of rewrite relations on \(\lambda\)-terms based on Girard's notion of reducibility

Uses Software

• Freshml
• FreshOCaml

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A theory of binding structures and applications to rewriting
• Adjunctions whose counits are coequalizers, and presentations of finitary enriched monads
• Variations on algebra: Monadicity and generalisations of equational theories
• The lambda calculus. Its syntax and semantics. Rev. ed.
• Termination of term rewriting: Interpretation and type elimination
• A fully abstract model for the \(\pi\)-calculus.
• Nominal logic, a first order theory of names and binding
• A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification
• The λ-calculus is ω-incomplete
• The lambda calculus is algebraic
• FreshML
• Computer Science Logic
• Computer Science Logic
• Functional and Logic Programming
• Programming Languages and Systems
• Automata, Languages and Programming
• On closed categories of functors
• Term Rewriting and Applications
• Inductive-data-type systems
• A typed context calculus

This page was built for publication: An initial algebra approach to term rewriting systems with variable binders