Now showing items 1-11 of 11

    • The Boehm-Jacopini Theorem is False, Propositionally 

      Kozen, Dexter; Tseng, Wei-Lung (Dustin) (2008-01-23)
      The Boehm-Jacopini theorem (Boehm and Jacopini, 1966) is a classical result of program schematology. It states that any deterministic flowchart program is equivalent to a while program. The theorem is usually formulated ...
    • A Coalgebraic Decision Procedure for NetKAT 

      Foster, Nate; Kozen, Dexter; Milano, Matthew; Silva, Alexandra; Thompson, Laure (2014-03-26)
      Program equivalence is a fundamental problem that has practical applications across a variety of areas of computing including compilation, optimization, software synthesis, formal verification, and many others. Equivalence ...
    • Completeness and Incompleteness in Nominal Kleene Algebra 

      Kozen, Dexter; Mamouras, Konstantinos; Silva, Alexandra (2014-11-14)
      Gabbay and Ciancia (2011) presented a nominal extension of Kleene algebra as a framework for trace semantics with dynamic allocation of resources, along with a semantics consisting of nominal languages. They also provided ...
    • Extensions Of Kleene Algebra For Program Verification 

      Mamouras, Konstantinos (2015-08-17)
      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 ...
    • KAT + B! 

      Grathwohl, Niels Bjørn Bugge; Kozen, Dexter; Mamouras, Konstantinos (2014-01-08)
      It is known that certain program transformations require a small amount of mutable state, a feature not explicitly provided by Kleene algebra with tests (KAT). In this paper we show how to axiomatically extend KAT with ...
    • Kleene Algebra with Equations 

      Kozen, Dexter; Mamouras, Konstantinos (2014-02-27)
      We identify sufficient conditions for the construction of free language models for systems of Kleene algebra with additional equations. The construction applies to a broad class of extensions of KA and provides a uniform ...
    • Left-Handed Completeness 

      Kozen, Dexter; Silva, Alexandra (2011-08-23)
      We give a new, significantly shorter proof of the completeness of the left-handed star rule of Kleene algebra. The proof reveals the rich interaction of algebra and coalgebra in the theory.
    • Nominal Kleene Coalgebra 

      Kozen, Dexter; Mamouras, Konstantinos; Petrisan, Daniela; Silva, Alexandra (2015-02-18)
      We develop the coalgebraic theory of nominal Kleene algebra, including an alternative language-theoretic semantics, a nominal extension of the Brzozowski derivative, and a bisimulation-based decision procedure for the ...
    • Nonlocal Flow of Control and Kleene Algebra with Tests 

      Kozen, Dexter (2008-04-11)
      Kleene algebra with tests (KAT) is an equational system for program verification that combines Kleene algebra (KA), or the algebra of regular expressions, with Boolean algebra. It can model basic programming and verification ...
    • On the Coalgebraic Theory of Kleene Algebra with Tests 

      Kozen, Dexter (2008-03-14)
      We develop a coalgebraic theory of Kleene algebra with tests (KAT) along the lines of Rutten (1998) for Kleene algebra (KA) and Chen and Pucella (2003) for a limited version of KAT, resolving two open problems of Chen and ...
    • Typed Kleene Algebra with Products and Iteration Theories 

      Kozen, Dexter; Mamouras, Konstantinos (2013-02-22)
      We develop a typed equational system that subsumes both iteration theories and typed Kleene algebra in a common framework. Our approach is based on cartesian categories endowed with commutative strong monads to handle ...