Equational Theories of Abnormal Termination Based on Kleene Algebra

DOI10.1007/978-3-662-54458-7_6zbMath1486.68043OpenAlexW2613020787MaRDI QIDQ2988362

Konstantinos Mamouras

Publication date: 19 May 2017

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-662-54458-7_6

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55) Semirings (16Y60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Equational classes, universal algebra in model theory (03C05)

Related Items

Semantic Foundations for Deterministic Dataflow and Stream Processing ⋮ Local completeness logic on Kleene algebra with tests

Uses Software

• NetKAT

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Partial derivatives of regular expressions and finite automaton constructions
• Notions of computation and monads
• A compositional natural semantics and Hoare logic for low-level languages
• A completeness theorem for Kleene algebras and the algebra of regular events
• On the completeness of propositional Hoare logic
• Combining effects: sum and tensor
• On formalised computer programs
• Probabilistic NetKAT
• Kleene Monads: Handling Iteration in a Framework of Generic Effects
• Synthesis of Strategies and the Hoare Logic of Angelic Nondeterminism
• Synthesis of Strategies Using the Hoare Logic of Angelic and Demonic Nondeterminism
• Nominal Kleene Coalgebra
• Completeness and Incompleteness in Nominal Kleene Algebra
• Handlers of Algebraic Effects
• Termination, deadlock, and divergence
• Hoare logic for Java in Isabelle/HOL
• On the Hoare theory of monadic recursion schemes
• Kleene Algebra with Equations
• Hoare-style reasoning with (algebraic) continuations
• The Hoare Logic of Deterministic and Nondeterministic Monadic Recursion Schemes
• NetKAT
• Derivatives of Regular Expressions
• Verification, Model Checking, and Abstract Interpretation