Extensions Of Kleene Algebra For Program Verification

Kleene algebra (KA) is an algebraic system that captures completely the laws of equivalence for regular expressions. It is also useful for reasoning about a multitude of computationally interesting structures. Of central interest in KA is a "star" operation that typically describes some kind of repetition or iteration. A combination of Kleene algebra with Boolean algebra has been proposed under the name of Kleene algebra with tests (KAT). This logical system can model the conventional programming constructs of imperative iterative programs, e.g. while loops and conditionals, and it has proven useful for various program verification tasks. In this dissertation we investigate variations and extensions of KA and KAT that are useful for program verification and for reasoning about mathematical structures that appear in computer science. At a technical level, we are interested in establishing completeness theorems, which assert that a proposed logical system is strong enough to capture all properties that are true in a mathematical structure or in a class of mathematical structures. Such results assure us of the quality of a logical system, and their proof often (certainly for the systems that we study here) reveals a systematic way of creating proof objects that certify properties of interest. The first part of this thesis explores generic extensions of KA and KAT with extra equational assumptions. Such extensions are meant to capture in the context of program verification some crucial properties of the domain of computation. We present a very general completeness meta-theorem that instantiates into several useful concrete completeness results. The second part focuses on extensions of KAT with extra mutable state that enable many useful semantics-preserving program transformations. The transformations we intend to cover are motivated by classical examples from the area of program schematology. We offer a rigorous and mathematically appealing algebraic approach, which replaces the typical combinatorial arguments about flowchart schemes with equational reasoning. Finally, a typed variation of KA is investigated that intends to capture properties of mathematical structures that appear in domain theory. The main result is that our proposed typed KA with products is strong enough to establish all the abstract properties of parametric fixpoints in the standard semantic model CPO, which is the category of [omega]-CPOs and [omega]-continuous maps.