Complete algebraic semantics for second-order rewriting systems based on abstract syntax with variable binding

DOI10.1017/S0960129522000287MaRDI QIDQ5058367zbMATH OpenOpenAlexFDO

Authors Makoto Hamana

Publication date 20 December 2022

Published in Mathematical Structures in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1017/s0960129522000287

zbMATH Keywords

term rewritinghigher-order abstract syntaxalgebraic modelsterminationhigher-order rewriting

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42) Semantics in the theory of computing (68Q55)

Recommendations

• Second-Order Algebraic Theories
• Term Rewriting and Applications
• An initial algebra approach to term rewriting systems with variable binders
• An algebraic structure for derivations in rewriting systems
• Second-Order Equational Logic (Extended Abstract)

Cites work

• scientific article; zbMATH DE number 1615229 (Why is no real title available?)
• scientific article; zbMATH DE number 2185657 (Why is no real title available?)
• scientific article; zbMATH DE number 996558 (Why is no real title available?)
• scientific article; zbMATH DE number 432742 (Why is no real title available?)
• scientific article; zbMATH DE number 3730111 (Why is no real title available?)
• scientific article; zbMATH DE number 3458870 (Why is no real title available?)
• scientific article; zbMATH DE number 1296290 (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 3367095 (Why is no real title available?)
• scientific article; zbMATH DE number 3400430 (Why is no real title available?)
• A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification
• A Unified Category-theoretic Semantics for Binding Signatures in Substructural Logics
• Deterministic second-order patterns
• Explicit substitutions with de bruijn's levels
• Free-algebra models for the \(\pi \)-calculus
• Functions-as-constructors Higher-order Unification
• Higher-order rewrite systems and their confluence
• How to prove decidability of equational theories with second-order computation analyser SOL
• Inductive-data-type systems
• Logic Based Program Synthesis and Transformation
• Multiversal Polymorphic Algebraic Theories: Syntax, Semantics, Translations, and Equational Logic
• Polymorphic Abstract Syntax via Grothendieck Construction
• Programming Languages and Systems
• Second-Order Algebraic Theories
• Second-Order Equational Logic (Extended Abstract)
• Term Rewriting and Applications
• Termination of rewrite relations on \(\lambda\)-terms based on Girard's notion of reducibility
• Termination of term rewriting: Interpretation and type elimination

Cited in

(5)

• Term Rewriting and Applications
• An algebraic structure for derivations in rewriting systems
• An initial algebra approach to term rewriting systems with variable binders
• Theory and practice of second-order rewriting: foundation, evolution, and SOL
• Sort-based confluence criteria for non-left-linear higher-order rewriting

Describes a project that uses

Uses Software

• Coq

This page was built for publication: Complete algebraic semantics for second-order rewriting systems based on abstract syntax with variable binding

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