JavaScript is disabled for your browser. Some features of this site may not work without it.
Browsing Computing and Information Science Technical Reports by Issue Date
Now showing items 1-20 of 307
-
Hedging a Portfolio of derivatives by Modeling Cost
(Cornell University, 2003-01-19)We consider the problem of hedging the loss of a given portfolio of derivatives using a set of more liquid derivative instruments. We illustrate why the typical mathematical formulation for this hedging problem is ... -
Herbivore: A Scalable and Efficient Protocol for Anonymous Communication
(Cornell University, 2003-01-28)Anonymity is increasingly important for networked applications amidst concerns over censorship and privacy. In this paper, we describe Herbivore, a peer-to-peer, scalable, tamper-resilient communication system that provides ... -
A Nuprl-PVS Connection: Integrating Libraries of Formal Mathematics.
(Cornell University, 2003-02-03)We describe a link between the Nuprl and PVS proof systems that enables users to access PVS from the Nuprl theorem proving environment, to import PVS theories into the Nuprl library, and to browse both Nuprl and PVS ... -
Automated Application-level Checkpointing of MPI Programs
(Cornell University, 2003-02-12)Because of increasing hardware and software complexity, the running time of many computational science applications is now more than the mean-time-to-failure of high-performance computing platforms. Therefore, computational ... -
Semi-supervised Clustering with User Feedback
(Cornell University, 2003-02-12)We present a new approach to clustering based on the observation that ``it is easier to criticize than to construct.'' Our approach of {\em semi-supervised clustering} allows a user to iteratively provide feedback to a ... -
A Logic of Events
(Cornell University, 2003-03-07)There is a well-established theory and practice for creating correct-by-construction functional programs by extracting them from constructive proofs of assertions of the form "For all x:A there exists y:B.R(x,y))." There ... -
Parametrized Tractability of Edge-Disjoint Paths on Directed Acyclic Graphs
(Cornell University, 2003-04-01)Given a graph and pairs $s_i t_i$ of terminals, the edge-disjoint paths problem is to determine whether there exist $s_i t_i$ paths that do not share any edges. We consider this problem on ditected acyclic graphs. It is ... -
Quantified Constraint Satisfaction Problems: Closure Properties, Complexity, and Proof Systems
(Cornell University, 2003-04-18)There has been much prior work on understanding the complexity of the constraint satisfaction problem (CSP), a broad framework capturing many combinatorial problems. This paper studies a natural and strict generalization ... -
On the Complexity of the Horn Theory of REL
(Cornell University, 2003-05-08)We show that the universal Horn theory of relational Kleene algebras is Pi-1-1-complete. -
A Linearly Typed Assembly Language
(Cornell University, 2003-06-04)Today's type-safe low-level languages rely on garbage collection to recycle heap-allocated objects safely. We present LTAL, a safe, low-level, yet simple language that ``stands on its own'': it guarantees safe execution ... -
First-Class Phantom Types
(Cornell University, 2003-07-10)Classical phantom types are datatypes in which type constraints are expressed using type variables that do not appear in the datatype cases themselves. They can be used to embed typed languages into Haskell or ML. ... -
Quantified Constraint Satisfaction and Small Commutative Conservative Operations
(Cornell University, 2003-07-22)The constraint satisfaction problem (CSP) is a broad framework capturing many combinatorial search problems. A natural and strict generalization of the CSP is the quantified constraint satisfaction problem (QCSP). The ... -
TeXQuery: A Full-Text Search Extension to XQuery (Part III: Use Cases Solutions)
(Cornell University, 2003-08-08)This report describes the TeXQuery use cases solutions. TeXQuery is a full-text search extension to XQuery. -
TeXQuery: A Full-Text Search Extension to XQuery (Part II: Formal Semantics)
(Cornell University, 2003-08-08)This report describes the formal semantics of TeXQuery. TeXQuery is a full-text search extension to XQuery. -
TeXQuery: A Full-Text Search Extension to XQuery (Part I: Language Specification)
(Cornell University, 2003-08-08)This report describes the TeXQuery language specification. TeXQuery is a full-text search extension to XQuery. -
KAT-ML: An Interactive Theorem Prover for Kleene Algebra with Tests
(Cornell University, 2003-08-21)KAT-ML is an interactive theorem prover for Kleene algebra with tests (KAT). The system is designed to reflect the natural style of reasoning with KAT that one finds in the literature. We describe the main features of ... -
Computability Classes for Enforcement Mechanisms
(Cornell University, 2003-08-26)A precise characterization of those security policies enforceable by program rewriting is given. This characterization exposes and rectifies problems in prior work on execution monitoring, yielding a more precise ... -
An Optimizing Compiler for Batches of Temporal Logic Formulas
(Cornell University, 2003-09-05)Model checking based on validating temporal logic formulas has proven practical and effective for numerous applications from verifying hardware designs to proving the correctness of software. As systems based on this ... -
TeXQuery: A Full-Text Search Extension to XQuery
(Cornell University, 2003-09-30)One of the key benefits of XML is its ability to represent a mix of structured and unstructured (text) data. Although current XML query languages such as XPath and XQuery can express rich queries over structured data, ... -
A comparison of eager and lazy class initialization in Java
(Cornell University, 2003-10-01)We prove that under some natural condition eager class initialization of a Java program P, as proposed in Kozen and Stillerman (2002), does not depend on the choice of a topological sort of the graph of class initialization ...
