POPL

This paper reports on the design and implementation of a practical shape analysis for C. The purpose of the analysis is to aid in the disambiguation of heap-allocated data structures by estimating the shape (Tree, DAG, or Cyclic Graph) of the data ...

This paper concerns the static analysis of programs that perform destructive updating on heap-allocated storage. We give an algorithm that conservatively solves this problem by using a finite shape-graph to approximate the possible "shapes" that heap-...

We present an interprocedural flow-insensitive points-to analysis based on type inference methods with an almost linear time cost complexity To our knowledge, this is the asymptotically fastest non-trivial interprocedural points-to analysis algorithm ...

We demonstrate the pragmatic value of the principal typing property, a property distinct from ML's principal type property, by studying a type system with principal typings. The type system is based on rank 2 intersection types and is closely related to ...

We study an extension of the Hindley/Milner system with explicit type scheme annotations and type declarations. The system can express polymorphic function arguments, user-defined data types with abstract components, and structure types with polymorphic ...

Module systems are a powerful, practical tool for managing the complexity of large software systems. Previous attempts to formulate a type-theoretic foundation for modular programming have been based on existential, dependent, or manifest types. These ...

Both software specifications and their intended properties can be expressed in a simple relational language. The claim that a specification satisfies a property becomes a relational formula that can be checked automatically by enumerating the formula's ...

Optimization and relaxation are two important operations that naturally arise in many applications involving constraints, e.g., engineering design, scheduling, decision support, etc. In optimization, we are interested in finding the optimal (i.e., best) ...

The aspect of purity versus impurity that we address involves the absence versus presence of mutation: the use of primitives (RPLACA and RPLACD in Lisp, set-car! and set-cdr! in Scheme) that change the state of pairs without creating new pairs. It is ...

We prove that the complexity of Lamping's optimal graph reduction technique for the λ-calculus can be exponential in the number of Lévy's family reductions. Starting from this consideration, we propose a new measure for what could be considered as "the ...

Dynamic code generation allows specialized code sequences to be created using runtime information. Since this information is by definition not available statically, the use of dynamic code generation can achieve performance inherently beyond that of ...

Specializing programs with respect to run-time invariants is an optimization technique that has shown to improve the performance of programs substantially. It allows a program to adapt to execution contexts that are valid for a limited time.Run-time ...

This paper presents program analyses and transformations that discover a general class of auxiliary information for any incremental computation problem. Combining these techniques with previous techniques for caching intermediate results, we obtain a ...

Region Inference is a technique for implementing programming languages that are based on typed call-by-value lambda calculus, such as Standard ML. The mathematical runtime model of region inference uses a stack of regions, each of which can contain an ...

A flow analysis framework for higher-order, mostly-functional languages is given. The framework unifies and extends previous work on flow analyses for this class of programming languages. The analysis is based on abstract interpretation and is ...

We present trace-based program analysts, a semantics-based framework for statically analyzing and transforming programs with loops, assignments, and nested record structures. Trace-based analyses are based on transfer transition, systems, which define ...

An important function of any register allocator is to target registers so as to eliminate copy instructions. Graph-coloring register allocation is an elegant approach to this problem. If the source and destination of a move instruction do not interfere, ...

Past register allocators have applied heuristics to allocate registers at the local, global, and interprocedural levels. This paper presents a polynomial time interprocedural register allocator that models the cost of allocating registers to procedures ...

We present a strikingly simple partial evaluator, that is type-directed and reifies a compiled program into the text of a residual, specialized program. Our partial evaluator is concise (a few lines) and it handles the flagship examples of offline ...

We show that a type system based on the intuitionistic modal logic S4 provides an expressive framework for specifying and analyzing computation stages in the context of functional languages. Our main technical result is a conservative embedding of ...

Closure conversion is a program transformation used by compilers to separate code from data. Previous accounts of closure conversion use only untyped target languages. Recent studies show that translating to typed target languages is a useful ...

We revisit the work of Paterson and of Meijer & Hutton, which describes how to construct catamorphisms for recursive datatype definitions that embed contravariant occurrences of the type being defined. Their construction requires, for each catamorphism, ...

Speculative evaluation, including leniency and futures, is often used to produce high degrees of parallelism, Existing speculative implementations, however, may serialize computation because of their implementation of queues of suspended threads. We ...

For a program with sufficient parallelism, reducing synchronization costs is one of the most important objectives for achieving efficient execution on any parallel machine. This paper presents a novel methodology for reducing synchronization costs of ...

We investigate functional computation as a special form of concurrent computation. As formal basis, we use a uniformly confluent core of the π-calculus, which is also contained in models of higher-order concurrent constraint programming. We embed the ...

We present a theory of types for concurrency based on a simple notion of typed algebras, and discuss its applications. The basic idea is to determine a partial algebra of processes by a partial algebra of types, thus controlling process composability, ...

The economy and flexibility of the pi-calculus make it attractive both as an object of theoretical study and as a basis for concurrent language design and implementation. However, such generality has a cost: encoding higher-level features like ...