2,199 papers · page 77 of 110
A flow analysis collects data-flow and control-flow information about programs. A compiler can use this information to enable optimizations. The analysis described in this article unifies and extends previous work on flow analyses for higher-order languages supporting assignment …
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 intrinsic complexity" of λ-…
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 unbounded number of values. …
We present trace-based program analysis, 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 the small-step operational se…
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 specialization is being active…
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 monovariant partial evaluation. …
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 Nielson & Nielson's two-level fu…
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 static code generation. Previo…
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, the definition of an anamo…
By adding reflexion to the chemical machine of Berry and Boudol, we obtain a formal model of concurrency that is consistent with mobility and distribution. Our model provides the foundations of a programming language with functional and object-oriented features. It can also be se…
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, then their nodes can be co…
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 structure accessible from each h…
Bisimilarity (also known as 'applicative bisimulation') has attracted a good deal of attention as an operational equivalence for λ-calculi. It approximates or even equals Morris-style contextual equivalence and admits proofs of program equivalence via co-induction. It has an elem…
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) solutions to a set of cons…
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 give a provably efficient para…
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 programs compiled for SPMD ex…
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, just as types in a typed app…
Article Generating machine specific optimizing compilers Share on Authors: Roger Hoover Computer Science Department, IBM TJ Watson Research Center, PO Box 704, Yorktown Heights, NY Computer Science Department, IBM TJ Watson Research Center, PO Box 704, Yorktown Heights, NYView Pr…
We have designed and implemented a type-based analysis for proving some basic properties of reactive systems. The analysis manipulates rich type expressions that contain information about the sizes of recursively defined data structures. Sized types are useful for detecting deadl…
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 interpretations. Because th…