POPL

The idiomatic APL programming style is limited by the constraints of a rectangular, homogeneous array as a data structure. Non-scalar data is difficult to represent and manipulate, and the non-scalar APL functions have no uniform extension to higher ...

This paper introduces the path, a new programming language construct designed to supplant the use of pointers to access and destructively update recursive data structures. In contrast to the complex semantics and proof rules for pointers, the semantics ...

We investigate the specialization of programs by means of program transformation techniques. There are two goals of this investigation: the construction of program synthesis tools, and a better understanding of the development of algorithms.By extending ...

This paper examines a number of programming primitives in query languages for relational databases. The basic framework is a language based on relational algebra, whose variables take relations as values. The primitives considered are (i) looping, (ii) ...

This paper examines "language processing" approach to paging where the of the programming language compiler or interpreter is responsible for generating the necessary control code for the page management of a program. We explore this idea for APL and ...

This paper describes the formal specifications of garbage collection in the programming language Cedar Mesa. They were developed as part of the process of identifying a safe subset of Mesa for which garbage collection was possible. The purpose of the ...

In this paper we describe how we have combined a number of tools (most of which understand a particular programming language) into a single system to aid in the reading, writing, and running of programs. We discuss the efficacy and the structure of our ...

A syntax-directed editor is a tool for structured program development. Such an editor can enforce syntactic correctness incrementally by restricting editing operations to legitimate modifications of the program's context-free derivation tree. However, ...

In analysis of programs and many other kinds of computation, algorithms are commonly written to have an input P and an output Q, where both P and Q are large and complicated objects. For example, P might be a routing problem and Q might be a solution to ...

This paper proposes a practical alternative to program verification -- called formal program testing -- with similar, but less ambitious goals. Like a program verifier, a formal testing system takes a program annotated with formal specifications as ...

It is shown that distributed systems of probabilistic processors are essentially more powerful than distributed systems of deterministic processors, i.e., there are certain useful behaviors that can be realized only by the former. This is demonstrated ...

Sufficient conditions are given for partial correctness assertions to determine the input-output semantics of quite general classes of programming languages. This determination cannot be unique unless states which are indistinguishable by predicates in ...

A theory of partial correctness proofs is formulated in Scott's logic computable junctions. This theory allows mechanical construction of verification condition solely on the basis of a denotational language definition. Extensionally these conditions, ...

When the "binding mechanisms" of assignment, quantification, and procedure definition are removed from a conventional first order total correctness logic of programs, the remaining logical system is decidable in time approximately one exponential in the ...

A temporal language and system are presented which are based on branching time structure. By the introduction of symmetrically dual sets of temporal operators, it is possible to discuss properties which hold either along one path or along all paths. ...

Verification of attribute grammar is discussed. As is widely recognized, attribute grammar of Knuth [8] is a very convenient device to describe semantics of programming languages, especially in automating compiler construction. Many efforts have been ...

Smalltalk is an object-oriented language designed and implemented by the Learning Research (Group of the Xerox Palo Alto Research Center [2, 5, 14]. Some features of this language are: abstract data classes, information inheritance by a superclass-subclass ...

Optimization of programs that may contain exception handling facilities requires new techniques. Program optimizations that do not account for exception handling facilities may incorrectly transform a procedure that can raise an exception, producing ...

Dependence graphs can be used as a vehicle for formulating and implementing compiler optimizations. This paper defines such graphs and discusses two kinds of transformations. The first are simple rewriting transformations that remove dependence arcs. ...

Data flow analysis is well understood at the intra-procedural level and efficient algorithms are available. When inter-procedural mechanisms such as recursion, procedure nesting, and pass-by-reference aliasing are introduced, the data flow problems ...