A unifying logical foundation for initial algebra semantics and induction

DOI10.1016/J.TCS.2026.115981MaRDI QIDQ7266644zbMATH OpenFDO

Authors Xiaohong Chen, Dorel Lucanu, Grigore Roşu

Publication date 15 June 2026

Published in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/J.TCS.2026.115981

zbMATH Keywords

inductive reasoninginitial algebramatching logic

Mathematics Subject Classification ID

Theory of computing (68Qxx)

Cites work

• A constructive algebraic hierarchy in Coq.
• A lattice-theoretical fixpoint theorem and its applications
• Automatic proofs by induction in theories without constructors
• CafeOBJ Report. The language, proof techniques, and methodologies for object-oriented algebraicspecification
• CASL: the Common Algebraic Specification Language.
• Coming to terms with quantified reasoning
• Constructing infinitary quotient-inductive types
• Constructors, sufficient completeness, and deadlock freedom of rewrite theories
• Formalization of universal algebra in Agda
• Foundational, compositional (co)datatypes for higher-order logic: category theory applied to theorem proving
• Higher inductive types as homotopy-initial algebras
• Homotopy-initial algebras in type theory
• scientific article; zbMATH DE number 3821084 (Why is no real title available?)
• scientific article; zbMATH DE number 3911679 (Why is no real title available?)
• scientific article; zbMATH DE number 3970817 (Why is no real title available?)
• scientific article; zbMATH DE number 4049024 (Why is no real title available?)
• scientific article; zbMATH DE number 18648 (Why is no real title available?)
• scientific article; zbMATH DE number 3804820 (Why is no real title available?)
• scientific article; zbMATH DE number 1424016 (Why is no real title available?)
• scientific article; zbMATH DE number 4189687 (Why is no real title available?)
• Inductionless induction
• Inductive types in homotopy type theory
• Initial Algebra Semantics Is Enough!
• Isabelle/HOL. A proof assistant for higher-order logic
• Matching -logic
• Matching logic
• Matching logic explained
• On the Algebraic Foundation of Proof Assistants for Intuitionistic Type Theory
• On the Completeness of Context-Sensitive Order-Sorted Specifications
• Packaging Mathematical Structures
• Quotients, inductive types, and quotient inductive types
• Representing inductively defined sets by wellorderings in Martin-Löf's type theory
• Results on the propositional \(\mu\)-calculus
• The algebraic specification of abstract data types
• Twenty years of rewriting logic
• Type classes for mathematics in type theory
• Über Möglichkeiten im Relativkalkül.
• Viper: a verification infrastructure for permission-based reasoning

Cited in

(1)

• A matching logic theory of multi-hole contexts

This page was built for publication: A unifying logical foundation for initial algebra semantics and induction

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