Now showing items 5-24 of 100

    • Capsules and Separation 

      Jeannin, Jean-Baptiste; Kozen, Dexter (2012-01-14)
      We study a formulation of separation logic using capsules, a representation of the state of a computation in higher-order programming languages with mutable variables. We prove soundness of the frame rule in this context ...
    • Certification of Compiler Optimizations using Kleene Algebra with Tests 

      Patron, Maria-Cristina; Kozen, Dexter (Cornell University, 1999-12)
      We use Kleene algebra with tests to verify a wide assortment of common compiler optimizations, including dead code elimination, common subexpression elimination, copy propagation, loop hoisting, induction variable elimination, ...
    • Church-Rosser Made Easy 

      Kozen, Dexter (2010-02-05)
      The Church-Rosser theorem states that the lambda-calculus is confluent under alpha- and beta-reductions. The standard proof of this result is due to Tait and Martin-Loef. In this note, we present an alternative proof ...
    • 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 ...
    • CoCaml: Programming with Coinductive Types 

      Jeannin, Jean-Baptiste; Kozen, Dexter; Silva, Alexandra (2012-12-31)
      We present CoCaml, a functional programming language extending OCaml, which allows us to define functions on coinductive datatypes parameterized by an equation solver. We provide numerous examples that attest to the ...
    • Coinductive Proof Principles for Stochastic Processes 

      Kozen, Dexter (Cornell University, 2005-03-24)
      We give an explicit coinduction principle for recursively-defined stochastic processes. The principle applies to any closed property, not just equality, and works even when solutions are not unique. We illustrate the use ...
    • Collective Inference on Markov Models for Modeling Bird Migration 

      Sheldon, Daniel; Elmohamed, M. A. Saleh; Kozen, Dexter (Cornell University, 2007-05-18)
      We investigate a family of inference problems on Markov models, where many sample paths are drawn from a Markov chain and partial information is revealed to an observer who attempts to reconstruct the sample paths. We ...
    • A Complete Gentzen-style Axiomatization for Set Constraints 

      Cheng, Allan; Kozen, Dexter (Cornell University, 1995-05)
      Set constraints are inclusion relations between expressions denoting sets of ground terms over a ranked alphabet. They are the main ingredient in set-based program analysis. In this paper we provide a Gentzen-style ...
    • 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 ...
    • A Completeness Theorem for Kleene Algebras and the Algebra of Regular Events 

      Kozen, Dexter (Cornell University, 1990-05)
      We give a finite axiomatization of the algebra of regular events involving only universal Horn formulas. Unlike Salomaa's axiomatizations, ours is sound for all interpretations over Kleene algebras.
    • Complexity of Finitely Presented Algebras 

      Kozen, Dexter (Cornell University, 1976-12)
      An algebra $\cal A$ is finitely presented if there is a finite set G of generator symbols, a finite set O of operator symbols, and a finite set $\Gamma$ of defining relations $x \equiv y$ where $x$ and $y$ are well-formed ...
    • The Complexity of Kleene Algebra with Tests 

      Cohen, Ernie; Kozen, Dexter; Smith, Frederick (Cornell University, 1996-07)
      Kleene algebras with tests provide a natural framework for equational specification and verification. Kleene algebras with tests and related systems have been used successfully in basic safety analysis, source-to-source ...
    • The Complexity of Set Constraints 

      Aiken, Alexander; Kozen, Dexter; Vardi, Moshe; Wimmers, Ed (Cornell University, 1993-05)
      Set constraints are relations between sets of terms. They have been used extensively in various applications in program analysis and type inference. We present several results on the computational complexity of solving ...
    • Computational Inductive Definability 

      Kozen, Dexter (Cornell University, 2002-04-03)
      It is shown that over any countable first-order structure, IND programs with dictionaries accept exactly the Pi-1-1 relations. This extends a result of Harel and Kozen (1984) relating IND and Pi-1-1 over countable structures ...
    • Computing the Newtonian Graph (Extended abstract) 

      Kozen, Dexter; Stefansson, Kjartan (Cornell University, 1993-10)
      A polynomial $f\in \complex[z]$ defines a vector field $N_f(z) = -f(z)/f'(z)$ on $\complex$. Certain degenerate curves of flow in $N_f$ give the edges of the Newtonian graph, as defined by \cite{Sma85}. These give ...
    • Computing with Capsules 

      Jeannin, Jean-Baptiste; Kozen, Dexter (2011-01-26)
      Capsules provide a clean algebraic representation of the state of a computation in higher-order functional and imperative languages. They play the same role as closures or heap- or stack-allocated environments but are ...
    • A Conversation with Dexter Kozen 

      Kozen, Dexter; Constable, Robert L. (Internet-First University Press, 2015-09-09)
      Kozen discusses his experiences at Cornell – his research and teaching experience, textbooks, participation in sports & music, etc.
    • Decidability of Systems of Set Constraints with Negative Constraints 

      Aiken, Alexander; Kozen, Dexter; Wimmers, Ed (Cornell University, 1993-06)
      Set constraints are relations between sets of terms. They have been used extensively in various applications in program analysis and type inference. Recently, several algorithms for solving general systems of positive ...
    • Decomposition of Algebraic Functions 

      Kozen, Dexter; Landau, Susan; Zippel, Richard (Cornell University, 1994-02)
      Functional decomposition--whether a function $f(x)$ can be written as a composition of functions $g(h(x))$ in a nontrivial way--is an important primitive in symbolic computation systems. The problem of univariate ...
    • Definability with Bounded Number of Bound Variables 

      Immerman, Neil; Kozen, Dexter (Cornell University, 1987-03)
      A theory satisfies the $k$-variable-property if every first-order formula is equivalent to a formula with at most $k$ bound variables (possibly reused). Gabbay has shown that a fixed time structure satisfies the $k$-variable ...