JavaScript is disabled for your browser. Some features of this site may not work without it.
Browsing Computing and Information Science by Type "technical report"
Now showing items 120 of 265

An Abstract Semantics for Atoms in Nuprl
Allen, Stuart F. (Cornell University, 20060605)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 ... 
AbstractionSafe Effect Handlers via Tunneling: Technical Report
Zhang, Yizhou (20181109)Algebraic effect handlers offer a unified approach to expressing controlflow transfer idioms such as exceptions, iteration, and async/await. Unfortunately, previous attempts to make these handlers typesafe have failed ... 
Accepting Blame: Expressive Checked Exceptions
Zhang, Yizhou; Salvaneschi, Guido; Beightol, Quinn; Liskov, Barbara; Myers, Andrew C. (201604)Unhandled exceptions crash programs, so a compiletime 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 ... 
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 ... 
Approximate Matching for PeertoPeer Overlays with Cubit
Wong, Bernard; Slivkins, Aleksandrs; Sirer, Emin Gun (20080519)Keyword search is a critical component in most content retrieval systems. Despite the emergence of completely decentralized and efficient peertopeer techniques for content distribution, there have not been similarly ... 
Approximate Matching for PeertoPeer Overlays with Cubit
Wong, Bernard; Slivkins, Alex; Sirer, Emin Gun (20081216)Keyword search is a critical component in most content retrieval systems. Despite the emergence of completely decentralized and efficient peertopeer techniques for content distribution, there have not been similarly ... 
Approximation Techniques for Spatial Data
Das, Abhinandan; Gehrke, Johannes; Riedewald, Mirek (Cornell University, 20040723)Spatial Database Management Systems (SDBMS), e.g., Geographical Information Systems, that manage spatial objects such as points, lines, and hyperrectangles, often have very high query processing costs. Accurate ... 
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 ... 
Automatic Measurement of Hardware Parameters for Embedded Processors
Yotov, Kamen; Pingali, Keshav; Stodghill, Paul (Cornell University, 20050126)Embedded processor designs are increasingly based on generalpurpose 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
Yotov, Kamen; Pingali, Keshav; Stodghill, Paul (Cornell University, 20041108)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
Worthington, James (Cornell University, 20070118)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
AboulHosn, Kamal (Cornell University, 20060531)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
Dilkina, Bistra; Gomes, Carla P.; Sabharwal, Ashish (20090409)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
Clarkson, Michael R.; Myers, Andrew C.; Schneider, Fred B. (Cornell University, 20050210)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 uncertaintybased approach ... 
Better than 1 Hop Lookup Performance with Proactive Caching
Ramasubramanian, Venugopalan; Sirer, Emin Gun (Cornell University, 20040218)High lookup latencies prohibit peertopeer overlays from being used in many performance intensive applications, even though they provide selforganization, scalability, and failure resilience. In this paper, we show ... 
BioDataBase
Lee, HuhnKie (Cornell University, 20050215)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
Sharp, Alexa (Cornell University, 20061011)In the area of extremal finite set theory there are many combinatorial results concerning the selection of m kelement 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
Schneider, Fred B. (20110524)A secure system must defend against all possible attacksincluding those unknown to the defender. But defenders, having limited resources, typically develop defenses only for attacks they know about. New kinds of attacks ... 
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 ... 
A Causal Logic of Events in Formalized Computational Type Theory
Bickford, Mark; Constable, Robert L. (Cornell University, 20051213)We provide a logic for distributed computing that has the explanatory and technical power of constructive logics of computation. Inparticular, we establish a proof technology that supports correctbyconstruction programming ...