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

ALEX  an Alexical Programming Language
Kozen, Dexter; Teitelbaum, Tim; Chen, Wilfred Z.; Field, John H.; Pugh, William W.; Vander Zanden, Bradley T. (Cornell University, 198705)ALEX is an experimental language for highlevel parallel programming. It is a testbed for exploring various nontraditional ways of expressing algorithmic ideas, making extensive use of highresolution color graphics. ... 
Applications of Metric Coinduction
Kozen, Dexter; Ruozzi, Nicholas (Cornell University, 20070516)Metric coinduction is a form of coinduction that can be used to establish properties of objects constructed as a limit of finite approximations. One proves a coinduction step showing that some property is preserved by one ... 
Automata on Guarded Strings and Applications
Kozen, Dexter (Cornell University, 20010125)Guarded strings are like ordinary strings over a finite alphabet P, except that atoms of the free Boolean algebra on a set of atomic tests B alternate with the symbols of P. The regular sets of guarded strings play the ... 
The BoehmJacopini Theorem is False, Propositionally
Kozen, Dexter; Tseng, WeiLung (Dustin) (20080123)The BoehmJacopini theorem (Boehm and Jacopini, 1966) is a classical result of program schematology. It states that any deterministic flowchart program is equivalent to a while program. The theorem is usually formulated ... 
Capsules and Separation
Jeannin, JeanBaptiste; Kozen, Dexter (20120114)We study a formulation of separation logic using capsules, a representation of the state of a computation in higherorder 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, MariaCristina; Kozen, Dexter (Cornell University, 199912)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, ... 
ChurchRosser Made Easy
Kozen, Dexter (20100205)The ChurchRosser theorem states that the lambdacalculus is confluent under alpha and betareductions. The standard proof of this result is due to Tait and MartinLoef. In this note, we present an alternative proof ... 
A Coalgebraic Decision Procedure for NetKAT
Foster, Nate; Kozen, Dexter; Milano, Matthew; Silva, Alexandra; Thompson, Laure (20140326)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, JeanBaptiste; Kozen, Dexter; Silva, Alexandra (20121231)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, 20050324)We give an explicit coinduction principle for recursivelydefined 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, 20070518)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 Gentzenstyle Axiomatization for Set Constraints
Cheng, Allan; Kozen, Dexter (Cornell University, 199505)Set constraints are inclusion relations between expressions denoting sets of ground terms over a ranked alphabet. They are the main ingredient in setbased program analysis. In this paper we provide a Gentzenstyle ... 
Completeness and Incompleteness in Nominal Kleene Algebra
Kozen, Dexter; Mamouras, Konstantinos; Silva, Alexandra (20141114)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, 199005)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, 197612)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 wellformed ... 
The Complexity of Kleene Algebra with Tests
Cohen, Ernie; Kozen, Dexter; Smith, Frederick (Cornell University, 199607)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, sourcetosource ... 
The Complexity of Set Constraints
Aiken, Alexander; Kozen, Dexter; Vardi, Moshe; Wimmers, Ed (Cornell University, 199305)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, 20020403)It is shown that over any countable firstorder structure, IND programs with dictionaries accept exactly the Pi11 relations. This extends a result of Harel and Kozen (1984) relating IND and Pi11 over countable structures ... 
Computing the Newtonian Graph (Extended abstract)
Kozen, Dexter; Stefansson, Kjartan (Cornell University, 199310)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, JeanBaptiste; Kozen, Dexter (20110126)Capsules provide a clean algebraic representation of the state of a computation in higherorder functional and imperative languages. They play the same role as closures or heap or stackallocated environments but are ...