An initial algebra approach to term rewriting systems with variable binders

DOI10.1007/S10990-006-8747-5MaRDI QIDQ853743zbMATH OpenOpenAlexFDO

Authors 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

Abstract syntax with variable bindingHigher-order abstract syntaxInitial algebra semanticsTerm rewriting systems

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Recommendations

• Complete algebraic semantics for second-order rewriting systems based on abstract syntax with variable binding
• Term Rewriting and Applications
• A theory of binding structures and applications to rewriting
• Initial algebras of terms with binding and algebraic structure
• Algebraic semantics of rewriting terms and types

Cites work

• A fully abstract model for the \(\pi\)-calculus.
• A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification
• A theory of binding structures and applications to rewriting
• A typed context calculus
• Adjunctions whose counits are coequalizers, and presentations of finitary enriched monads
• Automata, Languages and Programming
• Computer Science Logic
• Computer Science Logic
• FreshML: programming with binders made simple
• Functional and Logic Programming
• scientific article; zbMATH DE number 1612495 (Why is no real title available?)
• scientific article; zbMATH DE number 1722716 (Why is no real title available?)
• scientific article; zbMATH DE number 2185657 (Why is no real title available?)
• scientific article; zbMATH DE number 3730111 (Why is no real title available?)
• scientific article; zbMATH DE number 1086712 (Why is no real title available?)
• scientific article; zbMATH DE number 1759453 (Why is no real title available?)
• scientific article; zbMATH DE number 1833778 (Why is no real title available?)
• scientific article; zbMATH DE number 2111734 (Why is no real title available?)
• scientific article; zbMATH DE number 1405632 (Why is no real title available?)
• scientific article; zbMATH DE number 3227055 (Why is no real title available?)
• scientific article; zbMATH DE number 3400430 (Why is no real title available?)
• scientific article; zbMATH DE number 2242590 (Why is no real title available?)
• Inductive-data-type systems
• Nominal logic, a first order theory of names and binding
• On closed categories of functors
• Programming Languages and Systems
• Term Rewriting and Applications
• Termination of term rewriting: Interpretation and type elimination
• The lambda calculus is algebraic
• The lambda calculus. Its syntax and semantics. Rev. ed.
• The λ-calculus is ω-incomplete
• Variations on algebra: Monadicity and generalisations of equational theories

Cited in

(5)

• Size-based termination of higher-order rewriting
• Complete algebraic semantics for second-order rewriting systems based on abstract syntax with variable binding
• Initial algebras of terms with binding and algebraic structure
• Term Rewriting and Applications
• Termination of rewrite relations on \(\lambda\)-terms based on Girard's notion of reducibility

Describes a project that uses

Uses Software

• FreshOCaml
• FreshML

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

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