Now showing items 90-100 of 100

    • 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 ...
    • Set Constaints and Logic Programming 

      Kozen, Dexter (Cornell University, 1994-03)
      Set constraints are inclusion relations between expressions denoting sets of ground terms over a randed alphabet. They are the main ingredient in set-based program analysis[3,4,12,13,17,20,21,22,26]. In this paper we ...
    • Some Notes on Rational Spaces 

      Cheng, Allan; Kozen, Dexter (Cornell University, 1996-03)
      Set constraints are inclusions between expressions denoting set of ground terms over a finitely ranked alphabet $\Sigma$. Rational spaces are topological spaces obtained as spaces of runs of topological ...
    • Some Results in Dynamic Model Theory 

      Kozen, Dexter (Cornell University, 2002-10-31)
      First-order structures over a fixed signature S give rise to a family of trace-based and relational Kleene algebras with tests defined in terms of Tarskian frames. A Tarskian frame is a Kripke frame whose states are ...
    • Stone Duality for Markov Processes 

      Kozen, Dexter; Larsen, Kim G.; Mardare, Radu; Panangaden, Prakash (2013-03-14)
      We define Aumann algebras, an algebraic analog of probabilistic modal logic. An Aumann algebra consists of a Boolean algebra with operators modeling probabilistic transitions. We prove that countable Aumann algebras and ...
    • Strong Completeness for Markovian Logics 

      Kozen, Dexter; Mardare, Radu; Panangaden, Prakash (2013-06-14)
      In this paper we present Hilbert-style axiomatizations for three logics for reasoning about continuous-space Markov processes (MPs): (i) a logic for MPs defined for probability distributions on measurable state spaces, ...
    • A Theory of Interleavers 

      Andrews, Kenneth; Heegard, Chris; Kozen, Dexter (Cornell University, 1997-06)
      An interleaver is a hardware device commonly used in conjunction with error correcting codes to counteract the effect of burst errors. Interleavers are in widespread use and much is known about them from an engineering ...
    • Toward the Automation of Category Theory 

      Kozen, Dexter (Cornell University, 2004-09-08)
      We introduce a sequent system for basic category-theoretic reasoning suitable for computer implementation. We illustrate its use by giving a complete formal proof that the functor categories Fun[CxD,E] and Fun[C,Fun[D,E]] ...
    • Typed Kleene Algebra 

      Kozen, Dexter (Cornell University, 1998-03)
      In previous work we have found it necessary to argue that certain theorems of Kleene algebra hold even when the symbols are interpreted as nonsquare matrices. In this note we define and investigate typed Kleene algebra, ...
    • 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 ...
    • Well-Founded Coalgebras, Revisited 

      Jeannin, Jean-Baptiste; Kozen, Dexter; Silva, Alexandra (2013-05-24)
      Theoretical models of recursion schemes have been well studied under the names well-founded coalgebras, recursive coalgebras, corecursive algebras, and Elgot algebras. Much of this work focuses on conditions ensuring unique ...