The subtyping test consists of checking whether a type t is a descendant of a type r (Agrawal et al. 1989). We study how to perform such a test efficiently, assuming a dynamic hierarchy when new types are inserted at run-time. The goal is to achieve ...

Self-adjusting computation enables writing programs that can automatically and efficiently respond to changes to their data (e.g., inputs). The idea behind the approach is to store all data that can change over time in modifiable references and to let ...

Shape analyses are concerned with precise abstractions of the heap to capture detailed structural properties. To do so, they need to build and decompose summaries of disjoint memory regions. Unfortunately, many data structure invariants require ...

We describe a general technique for building abstract interpreters over powerful universally quantified abstract domains that leverage existing quantifier-free domains. Our quantified abstract domain can represent universally quantified facts like ∀i(0 ≤...

We present a framework for generating procedure summaries that are (a) precise - applying the summary in a given context yields the same result as re-analyzing the procedure in that context, and(b) concise - the summary exploits the commonalitiesin the ...

Software Transactional Memory (STM) is an attractive basis for the development of language features for concurrent programming. However, the semantics of these features can be delicate and problematic. In this paper we explore the tradeoffs between ...

An ad hoc data source is any semistructured data source for which useful data analysis and transformation tools are not readily available. Such data must be queried, transformed and displayed by systems administrators, computational biologists, ...

A lens is a bidirectional program. When read from left toright, it denotes an ordinary function that maps inputs to outputs. When read from right to left, it denotes an ''update translator'' that takes an input together with an updated output and ...

When scripts in untyped languages grow into large programs, maintaining them becomes difficult. A lack of types in typical scripting languages means that programmers must (re)discover critical pieces of design information every time they wish to change ...

Higher-order abstract syntax (HOAS) is a simple, powerful technique for implementing object languages, since it directly supports common and tricky routines dealing with variables, such as capture-avoiding substitution and renaming. This is achieved by ...

Focusing is a proof-search strategy, originating in linear logic, that elegantly eliminates inessential nondeterminism, with one byproduct being a correspondence between focusing proofs and programs with explicit evaluation order. Higher-order abstract ...

In language-based security, confidentiality and integrity policies conveniently specify the permitted flows of information between different parts of a program with diverse levels of trust. These policies enable a simple treatment of security, and they ...

GADTs are at the cutting edge of functional programming and becomemore widely used every day. Nevertheless, the semantic foundations underlying GADTs are not well understood. In this paper we solve this problem by showing that the standard theory of ...

This paper introduces a small but useful generalisation to the 'derivative' operation on datatypes underlying Huet's notion of 'zipper', giving a concrete representation to one-hole contexts in data which is undergoing transformation. This operator, '...

Communication is becoming one of the central elements in software development. As a potential typed foundation for structured communication-centred programming, session types have been studied over the last decade for a wide range of process calculi and ...

The C language definition leaves the sizes and layouts of types partially unspecified. When a C program makes assumptions about type layout, its semantics is defined only on platforms (C compilers and the underlying hardware) on which those assumptions ...

This paper presents a demand-driven, flow-insensitive analysisalgorithm for answering may-alias queries. We formulate thecomputation of alias queries as a CFL-reachability problem, and use this formulation to derive a demand-driven analysis algorithm. ...

This paper takes a fresh look at the problem of precise verification of heap-manipulating programs using first-order Satisfiability-Modulo-Theories (SMT) solvers. We augment the specification logic of such solvers by introducing the Logic of Interpreted ...

The search for proof and the search for counterexamples (bugs) are complementary activities that need to be pursued concurrently in order to maximize the practical success rate of verification tools.While this is well-understood in safety verification, ...

Okasaki and others have demonstrated how purely functional data structures that are efficient even in the presence of persistence can be constructed. To achieve good time bounds essential use is often made of laziness. The associated complexity analysis ...