JavaScript is disabled for your browser. Some features of this site may not work without it.
Browsing by Author "Kozen, Dexter"
Now showing items 7897 of 100

Parallel Resultant Computation
Ierardi, Doug J.; Kozen, Dexter (Cornell University, 199001)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, 199901)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, 198608)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 exponentialtime algorithms, both ... 
Practical Coinduction
Kozen, Dexter; Silva, Alexandra (20121111)Induction is a wellestablished proof principle that is taught in most undergraduate programs in mathematics and computer science. In computer science, it is used primarily to reason about inductivelydefined datatypes ... 
Probabilistic NetKAT
Foster, Nate; Kozen, Dexter; Mamouras, Konstantinos; Reitblatt, Mark; Silva, Alexandra (201507)This paper develops a new language for programming softwaredefined networks based on a probabilistic semantics. We extend the NetKAT language with new primitives for expressing probabilistic behaviors and enrich the ... 
Publication/Citation: A ProofTheoretic Approach to Mathematical Knowledge Management
Kozen, Dexter; Ramanarayanan, Ganesh (Cornell University, 20050316)There are many reallife 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, 199104)Rabin conditions are general class of properties of infinite sequences that emcompass most known automatatheoretic 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, 199501)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 (20110301)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 (20120731)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 (20151018)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
AboulHosn, Kamal; Kozen, Dexter (Cornell University, 20050718)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 ... 
SecondOrder Abstract Interpretation via Kleene Algebra
Kot, Lucja; Kozen, Dexter (Cornell University, 20041220)Most standard approaches to the static analysis of programs, such as the popular worklist method, are firstorder methods that inductively annotate program points with abstract values. In this paper we introduce a ... 
Set Constaints and Logic Programming
Kozen, Dexter (Cornell University, 199403)Set constraints are inclusion relations between expressions denoting sets of ground terms over a randed alphabet. They are the main ingredient in setbased 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, 199603)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, 20021031)Firstorder structures over a fixed signature S give rise to a family of tracebased 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 (20130314)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 (20130614)In this paper we present Hilbertstyle axiomatizations for three logics for reasoning about continuousspace 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, 199706)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, 20040908)We introduce a sequent system for basic categorytheoretic 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]] ...