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

\(\lambda \)-calculus\(\omega \)-algebraabstract reductionChurch-Rosser theoremsformal mathematicsKleene algebrarewritingsemiringstermination analysis

Mathematics Subject Classification ID

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

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

• 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
• 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?)
• 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

(15)

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

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)