Abstract abstract reduction
From MaRDI portal
Publication:817587
DOI10.1016/j.jlap.2005.04.001zbMath1086.68068OpenAlexW2045528636MaRDI QIDQ817587
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
rewritingsemiringsformal mathematicsKleene algebratermination analysis\(\lambda \)-calculus\(\omega \)-algebraabstract reductionChurch-Rosser theorems
Mechanization of proofs and logical operations (03B35) Grammars and rewriting systems (68Q42) Combinatory logic and lambda calculus (03B40)
Related Items (7)
Relation-Algebraic Verification of Prim’s Minimum Spanning Tree Algorithm ⋮ Algebraic coherent confluence and higher globular Kleene algebras ⋮ Algebraic notions of nontermination: Omega and divergence in idempotent semirings ⋮ Modal Tools for Separation and Refinement ⋮ Verifying minimum spanning tree algorithms with Stone relation algebras ⋮ An algebraic framework for minimum spanning tree problems ⋮ Automated verification of refinement laws
Cites Work
- Bi-rewrite systems
- Termination by completion
- A completeness theorem for Kleene algebras and the algebra of regular events
- A calculational approach to mathematical induction
- More Church-Rosser proofs (in Isabelle/HOL)
- Some lambda calculus and type theory formalized
- The variety of Kleene algebras with conversion is not finitely based
- A mechanical proof of the Church-Rosser theorem
- Completion of a Set of Rules Modulo a Set of Equations
- Regular Algebra Applied to Path-finding Problems
- On the union of well-founded relations
- Kleene algebra with domain
- Relational and Kleene-Algebraic Methods in Computer Science
- Parallel reductions in \(\lambda\)-calculus
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
This page was built for publication: Abstract abstract reduction