JavaScript is disabled for your browser. Some features of this site may not work without it.
Browsing Computing and Information Science Technical Reports by Title
Now showing items 1-20 of 307
-
An Abstract Semantics for Atoms in Nuprl
(Cornell University, 2006-06-05)We provide a supervaluating semantics for treating Atoms abstractly in Computational Type Theory, specifically for Nuprl logics. It supports a principled explanation for desirable gaps in provability without positing novel ... -
Abstraction-Safe Effect Handlers via Tunneling: Technical Report
(2018-11-09)Algebraic effect handlers offer a unified approach to expressing control-flow transfer idioms such as exceptions, iteration, and async/await. Unfortunately, previous attempts to make these handlers type-safe have failed ... -
Accepting Blame: Expressive Checked Exceptions
(2016-04)Unhandled exceptions crash programs, so a compile-time check that exceptions are handled should in principle make software more reliable. But designers of some recent languages have argued that the benefits of statically ... -
Achieving Reliability Through Distributed Data Flows and Recursive Delegation
(2009-03-15)Strong reliability properties, such as state machine replication or virtual synchrony, are hard to implement in a scalable manner. They are typically expressed in terms of global membership views. As we argue, global ... -
Applications of Metric Coinduction
(Cornell University, 2007-05-16)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 ... -
Approximate Matching for Peer-to-Peer Overlays with Cubit
(2008-05-19)Keyword search is a critical component in most content retrieval systems. Despite the emergence of completely decentralized and efficient peer-to-peer techniques for content distribution, there have not been similarly ... -
Approximate Matching for Peer-to-Peer Overlays with Cubit
(2008-12-16)Keyword search is a critical component in most content retrieval systems. Despite the emergence of completely decentralized and efficient peer-to-peer techniques for content distribution, there have not been similarly ... -
Approximation Techniques for Spatial Data
(Cornell University, 2004-07-23)Spatial Database Management Systems (SDBMS), e.g., Geographical Information Systems, that manage spatial objects such as points, lines, and hyper-rectangles, often have very high query processing costs. Accurate ... -
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 ... -
Automatic Measurement of Hardware Parameters for Embedded Processors
(Cornell University, 2005-01-26)Embedded processor designs are increasingly based on general-purpose processor families, modified and extended in various ways. However, the production of software for embedded processors remains a challenging problem. ... -
Automatic Measurement of Memory Hierarchy Parameters
(Cornell University, 2004-11-08)On modern computers, the running time of many applications is dominated by the cost of memory operations. To optimize such applications for a given platform, it is necessary to have a detailed knowledge of the memory ... -
Automatic Proof Generation in Kleene Algebra with Tests
(Cornell University, 2007-01-18)Kleene algebra (KA) is the algebra of regular events. Familiar examples of Kleene algebras include regular sets, relational algebras, and trace algebras. A Kleene algebra with tests (KAT) is a Kleene algebra with an ... -
An Axiomatization of Arrays for Kleene Algebra with Tests
(Cornell University, 2006-05-31)The formal analysis of programs with arrays is a notoriously difficult problem due largely to aliasing considerations. In this paper we augment the rules of Kleene algebra with tests (KAT) with rules for the equational ... -
Backdoors in the Context of Learning
(2009-04-09)The concept of backdoor variables has been introduced as a structural property of combinatorial problems that provides insight into the surprising ability of modern satisfiability (SAT) solvers to tackle extremely large ... -
Belief in Information Flow
(Cornell University, 2005-02-10)Measurement of information flow requires a definition of leakage, which traditionally has been defined to occur when an attacker's uncertainty about secret data is reduced. We show that this uncertainty-based approach ... -
Better than 1 Hop Lookup Performance with Proactive Caching
(Cornell University, 2004-02-18)High lookup latencies prohibit peer-to-peer overlays from being used in many performance intensive applications, even though they provide self-organization, scalability, and failure resilience. In this paper, we show ... -
BioDataBase
(Cornell University, 2005-02-15)This paper contains the concept of "Relational Taxonomy Tree (RTT)" and BioDataBase (BDB). RTT solves the following problems 1. how do we represent hierarchical entities like biological taxonomy? (section II and III in ... -
Birthdays, Broadcasts, and Boolean Algebras: Probabilistic Boolean Algebras and Applications
(Cornell University, 2006-10-11)In the area of extremal finite set theory there are many combinatorial results concerning the selection of m k-element sets. This type of set selection can also be viewed as a boolean algebra. In this paper we consider ... -
Blueprint for a Science of Cybersecurity
(2011-05-24)A secure system must defend against all possible attacks--including those unknown to the defender. But defenders, having limited resources, typically develop defenses only for attacks they know about. New kinds of attacks ... -
The Boehm-Jacopini Theorem is False, Propositionally
(2008-01-23)The Boehm-Jacopini 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 ...
