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

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]] ... 
Typed Kleene Algebra
Kozen, Dexter (Cornell University, 199803)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 (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 ... 
WellFounded Coalgebras, Revisited
Jeannin, JeanBaptiste; Kozen, Dexter; Silva, Alexandra (20130524)Theoretical models of recursion schemes have been well studied under the names wellfounded coalgebras, recursive coalgebras, corecursive algebras, and Elgot algebras. Much of this work focuses on conditions ensuring unique ...