An algebraic approach to computations with progress

DOI10.1016/j.jlamp.2015.11.009zbMath1344.68076OpenAlexW2252281036WikidataQ128988484 ScholiaQ128988484MaRDI QIDQ299188

Walter Guttmann

Publication date: 22 June 2016

Published in: Journal of Logical and Algebraic Methods in Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.jlamp.2015.11.009

zbMATH Keywords

relationsapproximation ordertracestimeaxiomatic program semanticsiteration algebras

Mathematics Subject Classification ID

Related Items

Relational characterisations of paths

Uses Software

• Nitpick
• Isabelle/HOL
• Sledgehammer

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Algebras for iteration and infinite computations
• Normal design algebra
• Kleene getting lazy
• Enabledness and termination in refinement algebra
• An algebra of hybrid systems
• Automated verification of refinement laws
• Relational algebraic semantics of deterministic and nondeterministic programs
• Reasoning algebraically about loops
• A completeness theorem for Kleene algebras and the algebra of regular events
• Isabelle/HOL. A proof assistant for higher-order logic
• Towards a refinement algebra
• Infinite executions of lazy and strict computations
• Completeness results for omega-regular algebras
• Unifying Lazy and Strict Computations
• Towards a Typed Omega Algebra
• Unifying Recursion in Partial, Total and General Correctness
• Conscriptions: A New Relational Model for Sequential Computations
• Unifying Theories of Programming That Distinguish Nontermination and Abort
• Automated Reasoning in Kleene Algebra
• The Linear Algebra of UTP
• Extending Sledgehammer with SMT Solvers
• Kleene algebra with domain
• Retrospective and Prospective for Unifying Theories of Programming
• Extended Conscriptions Algebraically
• Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder