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

DOI10.1017/S0960129522000287zbMATH Open1506.68044OpenAlexW4306153609MaRDI QIDQ5058367FDOQ5058367

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

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)

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)

Cites Work

• How to prove decidability of equational theories with second-order computation analyser SOL
• Termination of term rewriting: Interpretation and type elimination
• Free-algebra models for the \(\pi \)-calculus
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Higher-order rewrite systems and their confluence
• Title not available (Why is that?)
• Explicit substitutions with de bruijn's levels
• Title not available (Why is that?)
• A Unified Category-theoretic Semantics for Binding Signatures in Substructural Logics
• Title not available (Why is that?)
• Polymorphic Abstract Syntax via Grothendieck Construction
• Second-Order Equational Logic (Extended Abstract)
• A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification
• Inductive-data-type systems
• Title not available (Why is that?)
• Programming Languages and Systems
• Term Rewriting and Applications
• Termination of rewrite relations on \(\lambda\)-terms based on Girard's notion of reducibility
• Deterministic second-order patterns
• Second-Order Algebraic Theories
• Multiversal Polymorphic Algebraic Theories: Syntax, Semantics, Translations, and Equational Logic
• Functions-as-constructors Higher-order Unification
• Logic Based Program Synthesis and Transformation

Cited In (3)

• Term Rewriting and Applications
• An algebraic structure for derivations in rewriting systems
• Theory and practice of second-order rewriting: foundation, evolution, and SOL

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)