Now showing items 1-4 of 4

    • An Axiomatization of Arrays for Kleene Algebra with Tests 

      Aboul-Hosn, Kamal (Cornell University, 2006-05-31)
      The formal analysis of programs with arrays is a notoriously difficult problem due largely to aliasing considerations. In this paper we augment the rules of Kleene algebra with tests (KAT) with rules for the equational ...
    • KAT-ML: An Interactive Theorem Prover for Kleene Algebra with Tests 

      Aboul-Hosn, Kamal; Kozen, Dexter (Cornell University, 2003-08-21)
      KAT-ML is an interactive theorem prover for Kleene algebra with tests (KAT). The system is designed to reflect the natural style of reasoning with KAT that one finds in the literature. We describe the main features of ...
    • A Proof-Theoretic Approach to Mathematical Knowledge Management 

      Aboul-Hosn, Kamal (2006-12-08)
      Mathematics is an area of research that is forever growing. Definitions, theorems, axioms, and proofs are integral part of every area of mathematics. The relationships between these elements bring to light the elegant ...
    • Relational Semantics of Local Variable Scoping 

      Aboul-Hosn, Kamal; Kozen, Dexter (Cornell University, 2005-07-18)
      Most previous work on the equivalence of programs in the presence of local state has involved intricate memory modeling and the notion of contextual (observable) equivalence. We show how relational semantics can be used ...