Now showing items 12-31 of 100

• #### A Complete Gentzen-style Axiomatization for Set Constraints ﻿

(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 ﻿

(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 ﻿

(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 ﻿

(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 ﻿

(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 ﻿

(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 ﻿

(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) ﻿

(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 ﻿

(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 ﻿

(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 ﻿

(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 ﻿

(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 ﻿

(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 ...
• #### Eager Class Initialization for Java ﻿

(Cornell University, 2001-07-23)
We describe a static analysis method on Java bytecode to determine class initialization dependencies. This method can be used for eager class loading and initialization. It catches many initialization circularities that ...
• #### Efficient Algorithms for Optimal Video Transmission ﻿

(Cornell University, 1995-05)
This paper addresses the problem of sending an encoded video stream over a channel of limited bandwidth. When there is insufficient bandwidth available, some data must be dropped. For many video encodings, some data are ...
• #### Efficient Average-Case Algorithms for the Modular Group ﻿

(Cornell University, 1994-04)
The modular group occupies a central position in many branches of mathematical sciences. In this paper we give average polynomial-time algorithms for the unbounded and bounded membership problems for finitely generated ...
• #### Efficient Code Certification ﻿

(Cornell University, 1998-01)
We introduce a simple and efficient approach to the certification of compiled code. We ensure a basic but nontrivial level of code safety, including control flow safety, memory safety, and stack safety. The system is ...
• #### Efficient Resolution of Singularities of Plane Curves ﻿

(Cornell University, 1994-04)
We give a new algorithm for resolving singularities of plane curves. The algorithm is polynomial time in the bit complexity model, does not require factorization, and works over the rationals or finite fields.
• #### Equational Verification of Cache Blocking in LU Decomposition using Kleene Algebra with Tests ﻿

(Cornell University, 2002-10-24)
In a recent paper of Mateev et al. (2001), a new technique for program analysis called fractal symbolic analysis was introduced and applied to verify the correctness of a series of source-level transformations for cache ...
• #### Finitely Presented Algebras and the Polynomial Time Hiercharchy ﻿

(Cornell University, 1977-03)
Let $S_{n}(V_{n})=\{less than \Gamma, Q_{1}v_{1}\cdots Q_{k}v_{k} s \equiv j greater than | \Gamma$ is a finite presentation of $\cal A, Q_{1} \cdots Q_{k}$ is a string of quantifiers with $n$ alterations, the outermost ...