POPL

Data-flow analysis of scalar variables and data dependence analysis on array elements are two important program analyses used in optimizing and parallelizing compilers. Traditional data-flow analysis models accesses of array elements simply as accesses ...

Data-parallel languages like Fortran 90 express parallelism in the form of operations on data aggregates such as arrays. Misalignment of the operands of an array operation can reduce program performance on a distributed-memory parallel machine by ...

Although software pipelining has been proposed as one of the most important loop scheduling methods, simultaneous scheduling and register allocation is less understood and remains an open problem [28]. The objective of this paper is to develop a unified ...

We define an extension of the call-by-name lambda calculus with additional constructs and reduction rules that represent mutable variables and assignments. The extended calculus has neither a concept of an explicit store nor a concept of evaluation ...

According to folklore, Algol is an “orthogonal” extension of a simple imperative programming language with a call-by-name functional language. The former contains assignments, branching constructs, and compound statements; the latter is based on the ...

We present a new model, based on monads, for performing input/output in a non-strict, purely functional language. It is composable, extensible, efficient, requires no extensions to the type system, and extends smoothly to incorporate mixed-language ...

We present a new programming paradigm called Communicating Reactive Processes or CRP that unifies the capabilities of asynchronous and synchronous concurrent programming languages. Asynchronous languages such as CSP, OCCAM, or ADA are well-suited for ...

We propose a method to extend an ML-style polymorphic language with transparent communication primitives, and give their precise operational semantics. These primitives allow any polymorphic programs definable in ML to be used remotely in a manner ...

This paper presents the design and implementation of a “quasi real-time” garbage collector for Concurrent Caml Light, an implementation of ML with threads. This two-generation system combines a fast, asynchronous copying collector on the young ...

The continuation-passing style (CPS) transformation is powerful but complex. Our thesis is that this transformation is in fact compound, and we set out to stage it. We factor the CPS transformation into several steps, separating aspects in each step: (1)...

Mogensen has exhibited a very compact partial evaluator for the pure lambda calculus, using binding-time analysis followed by specialization. We give a correctness criterion for this partial evaluator and prove its correctness relative to this ...

We define an operational semantics for lazy evaluation which provides an accurate model for sharing. The only computational structure we introduce is a set of bindings which corresponds closely to a heap. The semantics is set at a considerably higher ...

A polymorphic function is parametric if its behavior does not depend on the type at which it is instantiated. Starting with Reynolds' work, the study of parametricity is typically semantic. In this paper, we develop a syntactic approach to parametricity,...

J. C. Reynolds suggested that Strachey's intuitive concept of “parametric” (i.e., uniform) polymorphism is closely linked to representation independence, and used logical relations to formalize this principle in languages with type variables and user-...

We consider the following problem in proving observational congruences in functional languages: given a call-by-name language based on the simply-typed λ-calculus with algebraic operations axiomatized by algebraic equations E, is the set of ...

Recursive data structures are abstractions of simple records and pointers. They impose a shape invariant, which is verified at compile-time and exploited to automatically generate code for building, copying, comparing, and traversing values without loss ...

We study the typing properties of CPS conversion for an extension of F_ω with control operators. Two classes of evaluation strategies are considered, each with call-by-name and call-by-value variants. Under the “standard” strategies, constructor ...

This article investigates an ML-like language with byname semantics for polymorphism: polymorphic objects are not evaluated once for all at generalization time, but re-evaluated at each specialization. Unlike the standard ML semantics, the by-name ...

We present practical approximation methods for computing interprocedural aliases and side effects for a program written in a language that includes pointers, reference parameters and recursion. We present the following results: 1) An algorithm for flow-...

We have designed and implemented an interprocedural program analyzer generator, called system Z. Our goal is to automate the generation and management of semantics-based interprocedural program analysis for a wide range of target languages.

System Z is ...

We describe and prove algorithms to convert programs which use the Parallel Computing Forum Parallel Sections construct into Static Single Assignment (SSA) form. This proces allows compilers to apply classical scalar optimization algorithms to ...

In this paper we introduce a statically-typed, functional, object-oriented programming language, TOOPL, which supports classes, objects, methods, instance variable, subtypes, and inheritance.

It has proved to be surprisingly difficult to design ...

It is widely agreed that recursive types are inherent in the static typing of the essential mechanisms of object-oriented programming: encapsulation, message passing, subtyping, and inheritance. We demonstrate here that modeling object encapsulation in ...

We show how a higher order logic, the calculus of constructions, can be used to give a simple, first principles treatment of record calculi, polymorphism, and subtyping. The development follows the constructive idiom of extracting implementations of ...

Central to constraint logic programming (CLP) languages is the notion of a global constraint solver which is queried to direct execution and to which constraints are monotonically added. We present a methodology for use in the compilation of CLP ...

We present in this paper a structure–sharing framework originally developed for a Dynamic Programming interpreter of Logic programs called DyALog. This mechanism should be of interest for alternative execution models of PROLOG which maintain multiple ...