7,482 papers · page 318 of 375
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 equationally specified program…
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 languages which is designed to red…
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 to the entire array, and is…
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 algorithmic framework for …
We study the type inference problem for a system with type classes as in the functional programming language Haskell. Type classes are an extension of ML-style polymorphism with overloading. We generalize Milner's work on polymorphism by introducing a separate context constrainin…
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-defined types. Here, we use r…
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 order; nevertheless, we show th…
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 completely transparent to the pr…
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 terms of existential types …
In many kinds of emnputatiomd contexts, modifications of the input data are to be processed at once so as to have immediate effect on the output. Because small changes in the input to a computation often cause only small changes in the outpu~ the challenge is to compute the new o…
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 observational congruences between terms…
No abstract available.
To separately compile a program module in traditional statically-typed languages, one has to manually write down an import interface which explicitly specifies all the external symbols referenced in the module. Whenever the definitions of these external symbols are changed, the m…
No abstract available.
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 explicitly parallel programs. To do …
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 specification. We show that the conv…
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 typed λ-calculus. In an attemp…
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.
No abstract available.
An efficient mechanism for method lookup is csscntial in any reasonable implementation of a clussbased object-oriented language.One tcchniquc, static caches, provide constant time lookup, but consumes cxcessive memory.To alleviate the memory consumption problem many systems USC a…