JavaScript is disabled for your browser. Some features of this site may not work without it.
Browsing by Subject "Kleene algebra"
Now showing items 111 of 11

The BoehmJacopini Theorem is False, Propositionally
Kozen, Dexter; Tseng, WeiLung (Dustin) (20080123)The BoehmJacopini 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 (20140326)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 (20141114)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 (20150817)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 (20140108)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 (20140227)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 ... 
LeftHanded Completeness
Kozen, Dexter; Silva, Alexandra (20110823)We give a new, significantly shorter proof of the completeness of the lefthanded 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 (20150218)We develop the coalgebraic theory of nominal Kleene algebra, including an alternative languagetheoretic semantics, a nominal extension of the Brzozowski derivative, and a bisimulationbased decision procedure for the ... 
Nonlocal Flow of Control and Kleene Algebra with Tests
Kozen, Dexter (20080411)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 (20080314)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 (20130222)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 ...