Abstract abstract reduction

DOI10.1016/J.JLAP.2005.04.001MaRDI QIDQ817587zbMATH OpenOpenAlexFDO

Authors Georg Struth

Publication date 16 March 2006

Published in The Journal of Logic and Algebraic Programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.jlap.2005.04.001

zbMATH Keywords

rewritingformal mathematicssemiringsKleene algebra\(\lambda \)-calculustermination analysis\(\omega \)-algebraabstract reductionChurch-Rosser theorems

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42) Mechanization of proofs and logical operations (03B35) Combinatory logic and lambda calculus (03B40)

Recommendations

• scientific article; zbMATH DE number 1953901
• scientific article; zbMATH DE number 4047065
• Formal proofs about rewriting using ACL2
• TERMINATION OF ABSTRACT REDUCTION SYSTEMS
• scientific article; zbMATH DE number 3934390

Cites work

• scientific article; zbMATH DE number 1612485 (Why is no real title available?)
• scientific article; zbMATH DE number 1696821 (Why is no real title available?)
• scientific article; zbMATH DE number 3131080 (Why is no real title available?)
• scientific article; zbMATH DE number 3875232 (Why is no real title available?)
• scientific article; zbMATH DE number 5604075 (Why is no real title available?)
• scientific article; zbMATH DE number 4007716 (Why is no real title available?)
• scientific article; zbMATH DE number 4047065 (Why is no real title available?)
• scientific article; zbMATH DE number 45228 (Why is no real title available?)
• scientific article; zbMATH DE number 3497806 (Why is no real title available?)
• scientific article; zbMATH DE number 2163052 (Why is no real title available?)
• scientific article; zbMATH DE number 1889386 (Why is no real title available?)
• scientific article; zbMATH DE number 234018 (Why is no real title available?)
• scientific article; zbMATH DE number 3316966 (Why is no real title available?)
• scientific article; zbMATH DE number 3366846 (Why is no real title available?)
• A calculational approach to mathematical induction
• A completeness theorem for Kleene algebras and the algebra of regular events
• A mechanical proof of the Church-Rosser theorem
• Bi-rewrite systems
• Completion of a Set of Rules Modulo a Set of Equations
• Kleene algebra with domain
• More Church-Rosser proofs (in Isabelle/HOL)
• On the union of well-founded relations
• Parallel reductions in \(\lambda\)-calculus
• Regular Algebra Applied to Path-finding Problems
• Relational and Kleene-Algebraic Methods in Computer Science
• Some lambda calculus and type theory formalized
• Termination by completion
• The variety of Kleene algebras with conversion is not finitely based

Cited in

(14)

• Algebraic characterizations for reduction systems
• Abstract blowing down
• scientific article; zbMATH DE number 2086962 (Why is no real title available?)
• scientific article; zbMATH DE number 1953901 (Why is no real title available?)
• An algebraic framework for minimum spanning tree problems
• Structures for abstract rewriting
• Modal tools for separation and refinement
• An abstract formulation for rewrite systems
• Algebraic notions of nontermination: Omega and divergence in idempotent semirings
• Verifying minimum spanning tree algorithms with Stone relation algebras
• Algebraic coherent confluence and higher globular Kleene algebras
• Relation-algebraic verification of Prim's minimum spanning tree algorithm
• Abstract strategies and coherence
• Automated verification of refinement laws

This page was built for publication: Abstract abstract reduction

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