Now showing items 1-10 of 10

  • 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 ...
  • 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 ...