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 120 of 307

Hedging a Portfolio of derivatives by Modeling Cost
Boyle, Katharyn A.; Coleman, Thomas F.; Li, Yuying (Cornell University, 20030119)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
Goel, Sharad; Robson, Mark; Polte, Milo; Sirer, Emin (Cornell University, 20030128)Anonymity is increasingly important for networked applications amidst concerns over censorship and privacy. In this paper, we describe Herbivore, a peertopeer, scalable, tamperresilient communication system that provides ... 
A NuprlPVS Connection: Integrating Libraries of Formal Mathematics.
Allen, Stuart F.; Bickford, Mark; Constable, Robert; Eaton, Richard; Kreitz, Christoph. (Cornell University, 20030203)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 ... 
Semisupervised Clustering with User Feedback
Cohn, David; Caruana, Rich; McCallum, Andrew (Cornell University, 20030212)We present a new approach to clustering based on the observation that ``it is easier to criticize than to construct.'' Our approach of {\em semisupervised clustering} allows a user to iteratively provide feedback to a ... 
Automated Applicationlevel Checkpointing of MPI Programs
Bronevetsky, Greg; Marques, Daniel; Pingali, Keshav; Stodghill, Paul (Cornell University, 20030212)Because of increasing hardware and software complexity, the running time of many computational science applications is now more than the meantimetofailure of highperformance computing platforms. Therefore, computational ... 
A Logic of Events
Bickford, Mark; Constable, Robert L. (Cornell University, 20030307)There is a wellestablished theory and practice for creating correctbyconstruction 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 EdgeDisjoint Paths on Directed Acyclic Graphs
Slivkins, Aleksandrs (Cornell University, 20030401)Given a graph and pairs $s_i t_i$ of terminals, the edgedisjoint 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
Chen, Hubie (Cornell University, 20030418)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
Hardin, Chris; Kozen, Dexter (Cornell University, 20030508)We show that the universal Horn theory of relational Kleene algebras is Pi11complete. 
A Linearly Typed Assembly Language
Cheney, James; Morrisett, Greg (Cornell University, 20030604)Today's typesafe lowlevel languages rely on garbage collection to recycle heapallocated objects safely. We present LTAL, a safe, lowlevel, yet simple language that ``stands on its own'': it guarantees safe execution ... 
FirstClass Phantom Types
Cheney, James; Hinze, Ralf (Cornell University, 20030710)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
Chen, Hubie (Cornell University, 20030722)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 FullText Search Extension to XQuery (Part III: Use Cases Solutions)
AmerYahia, Sihem; Botev, Chavdar; Robie, Jonathan; Shanmugasundaram, Jayavel (Cornell University, 20030808)This report describes the TeXQuery use cases solutions. TeXQuery is a fulltext search extension to XQuery. 
TeXQuery: A FullText Search Extension to XQuery (Part I: Language Specification)
AmerYahia, Sihem; Botev, Chavdar; Robie, Jonathan; Shanmugasundaram, Jayavel (Cornell University, 20030808)This report describes the TeXQuery language specification. TeXQuery is a fulltext search extension to XQuery. 
TeXQuery: A FullText Search Extension to XQuery (Part II: Formal Semantics)
AmerYahia, Sihem; Botev, Chavdar; Robie, Jonathan; Shanmugasundaram, Jayavel (Cornell University, 20030808)This report describes the formal semantics of TeXQuery. TeXQuery is a fulltext search extension to XQuery. 
KATML: An Interactive Theorem Prover for Kleene Algebra with Tests
AboulHosn, Kamal; Kozen, Dexter (Cornell University, 20030821)KATML 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
Hamlen, Kevin W.; Morrisett, Greg; Schneider, Fred B. (Cornell University, 20030826)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
Ezick, James (Cornell University, 20030905)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 FullText Search Extension to XQuery
AmerYahia, Sihem; Botev, Chavdar; Shanmugasundaram, Jayavel (Cornell University, 20030930)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
Dziobiak, Stanislaw M. (Cornell University, 20031001)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 ...