POPL

Standard ML is a useful programming language with polymorphic expressions and a flexible module facility. One notable feature of the expression language is an algorithm which allows type information to be omitted. We study the implicitly-typed ...

We present a new approach to programming languages for parallel computers that uses an effect system to discover expression scheduling constraints. This effect system is part of a 'kinded' type system with three base kinds: types, which describe the ...

We extend the functional language ML by allowing the recursive calls to a function F on the right-hand side of its definition to be at different types, all generic instances of the (derived) type of F on the left-hand side of its definition. The ...

A denotational semantic definition of SMALLTALK-80 is given. Its most notable characteristic is a surprisingly simple treatment of inheritance. An executable version of the semantics, written in STANDARD ML, is also described.

We give an algorithm for type inference in a language with functions, records, and variant records. A similar language was studied by Cardelli who gave a type checking algorithm. This language is interesting because it captures aspects of object-...

For a typed λ-calculus we develop an algorithm that, given some partial information about what must happen at run-time, will work out what actually can be computed at compile-time and what must be deferred to run-time.

A collecting interpretation of expressions is an interpretation of a program that allows one to answer questions of the sort: “What are all possible values to which an expression might evaluate during program execution?” Answering such questions in a ...

Analyzing time complexity of functional programs in a lazy language is problematic, because the time required to evaluate a function depends on how much of the result is “needed” in the computation. Recent results in strictness analysis provide a ...

The need to integrate several versions of a program into a common one arises frequently, but it is a tedious and time consuming task to integrate programs by hand. The main contribution of this paper is an algorithm, called integrate, that takes as ...

Program dependence graphs were introduced by Kuck as an intermediate program representation well suited for performing optimizations, vectorization, and parallelization. There are also additional applications for them as an internal program ...

The designers of (functional) programming languages are faced with two occasionally conflicting goals: programmer convenience and semantic simplicity. For example, it is convenient to treat I/O operations as primitive “functions” with side effects, but ...

An analysis of the λ_ugr;-C-calculus and its problematic relationship to operational equivalence leads to a new control facility: the prompt-application. With the introduction of prompt-applications, the control calculus becomes a traditional calculus ...

The Store Model of Halpern-Meyer-Trakhtenbrot is shown—after suitable repair—to be a fully abstract model for a limited fragment of ALGOL in which procedures do not take procedure parameters. A simple counter-example involving a parameter of program ...

Three semantics-preserving transformations (static replacement, factoring, and combinator selection) are used to convert a continuation semantics into a formal description of a semantic analyzer and code generator. The result of this derivation is a ...

Rewriting techniques have been used to reason about a variety of topics related to programming languages, e.g., abstract data types, Petri Nets, FP programs, and data bases. They have also been used in the implementation and definition of a variety of ...

Bisimulation is the primitive notion of equivalence between concurrent processes in Milner's Calculus of Communicating Systems (CCS); there is a nontrivial game-like protocol for distinguishing nonbisimular processes. In contrast, process ...

A general definition of the notion of superimposition is presented. We show that previous constructions under the same name can be seen as special cases of our definition. We consider several properties of superimposition definable in our terms, notably ...

Two distinct extensions of temporal logic has been recently advocated in the literature. The first extension is the addition of fixpoint operators that enable the logic to make assertions about arbitrary regular events. The second extension is the ...

We investigate a framework for efficient flow analyses of logic programs. A major problem in this context is that unification can give rise to aliasing and dependencies between variables whose effects are difficult to predict, and which make sound flow ...

We present an algorithm for updating data flow information derived from a program, in response to program edits. Our algorithm, applicable to intraprocedural or interprocedural data flow problems, is more general than previous methods because it can ...

The choice of binding time disciplines has major consequences for both the run-time efficiency of programs and the convenience of the language expressing algorithms. Late storage binding time, dynamic allocation, provides the flexibility necessary to ...

A Rewrite System is a collection of rewrite rules of the form α β where α and β are tree patterns. A rewrite system can be extended by associating a cost with each rewrite rule, and by defining the cost of a rewrite sequence as the sum of the costs of ...

A programmable systolic array of high-performance cells is an attractive computation engine if it attains the same utilization of dedicated arrays of simple cells. However, typical implementation techniques used in high-performance processors, such as ...

Supercompilers must reschedule computations defined by nested DO-loops in order to make an efficient use of supercomputer features (vector units, multiple elementary processors, cache memory, etc…). Many rescheduling techniques like loop interchange, ...