Now showing items 71-90 of 100

    • On the Completeness of Propositional Hoare Logic 

      Kozen, Dexter; Tiuryn, Jerzy (Cornell University, 1999-09)
      We investigate the completeness of Hoare Logic on the propositional level. In particular, the expressiveness requirements of Cook's proof are characterized propositionally. We give a completeness result for Propositional ...
    • On the Complexity of Reasoning in Kleene Algebra 

      Kozen, Dexter (Cornell University, 1997-03)
      We study the complexity of reasoning in Kleene algebra and *-continuous Kleene algebra in the presence of extra equational assumptions $E$; that is, the complexity of deciding the validity of universal Horn formulas $E\imp ...
    • On the Complexity of the Horn Theory of REL 

      Hardin, Chris; Kozen, Dexter (Cornell University, 2003-05-08)
      We show that the universal Horn theory of relational Kleene algebras is Pi-1-1-complete.
    • On the Elimination of Hypotheses in Kleene Algebra with Tests 

      Hardin, Chris; Kozen, Dexter (Cornell University, 2002-10-21)
      The validity problem for certain universal Horn formulas of Kleene algebra with tests (KAT) can be efficiently reduced to the equational theory. This reduction is known as elimination of hypotheses. Hypotheses are used ...
    • On the Representation of Kleene Algebras with Tests 

      Kozen, Dexter (Cornell University, 2003-10-06)
      We investigate conditions under which a given Kleene algebra with tests is isomorphic to an algebra of binary relations. Two simple separation properties are identified that, along with star-continuity, are sufficient ...
    • On Two Letters versus Three 

      Kozen, Dexter (Cornell University, 2002-02-04)
      If A is a context-free language over a two-letter alphabet, then the set of all words obtained by sorting words in A and the set of all permutations of words in A are context-free. This is false over alphabets of three ...
    • Optimal Coin Flipping 

      Kozen, Dexter (2009-06-02)
      This paper studies the problem of simulating a coin of arbitrary real bias q with a coin of arbitrary real bias p with minimum loss of entropy. We establish a lower bound that is strictly greater than the information-theoretic ...
    • Parallel Resultant Computation 

      Ierardi, Doug J.; Kozen, Dexter (Cornell University, 1990-01)
      A resultant is a purely algebraic criterion for determining when a finite collection of polynomials have a common zero. It has been shown to be a useful tool in the design of efficient parallel and sequential algorithms ...
    • Parikh's Theorem in Commutative Kleene Algebra 

      Hopkins, Mark; Kozen, Dexter (Cornell University, 1999-01)
      Parikh's Theorem says that the commutative image of every context free language is the commutative image of some regular set. Pilling has shown that this theorem is essentially a statement about least solutions of ...
    • Polynomial Decomposition Algorithms 

      Kozen, Dexter; Landau, Susan (Cornell University, 1986-08)
      In a recent paper [BZ], Barton and Zippel examine the question of when a polynomial $f(x)$ over a field of characteristic 0 has a nontrivial decomposition $f(x)=g(h(x))$. They give two exponential-time algorithms, both ...
    • Practical Coinduction 

      Kozen, Dexter; Silva, Alexandra (2012-11-11)
      Induction is a well-established proof principle that is taught in most undergraduate programs in mathematics and computer science. In computer science, it is used primarily to reason about inductively-defined datatypes ...
    • Probabilistic NetKAT 

      Foster, Nate; Kozen, Dexter; Mamouras, Konstantinos; Reitblatt, Mark; Silva, Alexandra (2015-07)
      This paper develops a new language for programming software-defined networks based on a probabilistic semantics. We extend the NetKAT language with new primitives for expressing probabilistic behaviors and enrich the ...
    • Publication/Citation: A Proof-Theoretic Approach to Mathematical Knowledge Management 

      Kozen, Dexter; Ramanarayanan, Ganesh (Cornell University, 2005-03-16)
      There are many real-life examples of formal systems that support constructions or proofs, but that do not provide direct support for remembering them so that they can be recalled and reused in the future. In this paper ...
    • Rabin Measures and Their Applications to Fairness and Automata Theory 

      Klarlund, Nils; Kozen, Dexter (Cornell University, 1991-04)
      Rabin conditions are general class of properties of infinite sequences that emcompass most known automata-theoretic acceptance conditions and notions of fairness. In this paper we show how to determine whether a program ...
    • Rational Spaces and Set Constraints 

      Kozen, Dexter (Cornell University, 1995-01)
      Set constraints are inclusions between expressions denoting sets of ground terms. They have been used extensively in program analysis and type inference. In this paper we investigate the topological structure of the spaces ...
    • Realization of Coinductive Types 

      Kozen, Dexter (2011-03-01)
      We give an explicit combinatorial construction of final coalgebras for a modest generalization of polynomial functors on Set. Type signatures are modeled as directed multigraphs instead of endofunctors. The final coalgebra ...
    • Reflection in the Chomsky Hierarchy 

      Barendregt, Henk; Capretta, Venanzio; Kozen, Dexter (2012-07-31)
      We investigate which classes of formal languages in the Chomsky hierarchy are reflexive, that is, contain a language of codes that is universal for the whole class.
    • Regular Expressions with Dynamic Name Binding 

      Kozen, Dexter; Milius, Stefan; Schröder, Lutz; Wißmann, Thorsten (2015-10-18)
      Nominal Kleene algebra (NKA) is a formalism to specify trace languages with name generation; it extends standard regular expressions with a name binding construct. NKA has been proved complete over a natural nominal language ...
    • 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 ...
    • Second-Order Abstract Interpretation via Kleene Algebra 

      Kot, Lucja; Kozen, Dexter (Cornell University, 2004-12-20)
      Most standard approaches to the static analysis of programs, such as the popular worklist method, are first-order methods that inductively annotate program points with abstract values. In this paper we introduce a ...