Now showing items 1-20 of 307

    • An Abstract Semantics for Atoms in Nuprl 

      Allen, Stuart F. (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 

      Zhang, Yizhou (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 

      Zhang, Yizhou; Salvaneschi, Guido; Beightol, Quinn; Liskov, Barbara; Myers, Andrew C. (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 

      Ostrowski, Krzysztof; Birman, Ken; Dolev, Danny; Sakoda, Chuck (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 

      Kozen, Dexter; Ruozzi, Nicholas (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 

      Wong, Bernard; Slivkins, Aleksandrs; Sirer, Emin Gun (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 

      Wong, Bernard; Slivkins, Alex; Sirer, Emin Gun (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 

      Das, Abhinandan; Gehrke, Johannes; Riedewald, Mirek (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 

      Bronevetsky, Greg; Marques, Daniel; Pingali, Keshav; Stodghill, Paul (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 

      Yotov, Kamen; Pingali, Keshav; Stodghill, Paul (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 

      Yotov, Kamen; Pingali, Keshav; Stodghill, Paul (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 

      Worthington, James (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 

      Aboul-Hosn, Kamal (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 

      Dilkina, Bistra; Gomes, Carla P.; Sabharwal, Ashish (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 

      Clarkson, Michael R.; Myers, Andrew C.; Schneider, Fred B. (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 

      Ramasubramanian, Venugopalan; Sirer, Emin Gun (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 

      Lee, Huhn-Kie (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 

      Sharp, Alexa (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 

      Schneider, Fred B. (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 

      Kozen, Dexter; Tseng, Wei-Lung (Dustin) (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 ...