skip to main content
10.1145/567067acmconferencesBook PagePublication PagespoplConference Proceedingsconference-collections
POPL '83: Proceedings of the 10th ACM SIGACT-SIGPLAN symposium on Principles of programming languages
ACM1983 Proceeding
Publisher:
  • Association for Computing Machinery
  • New York
  • NY
  • United States
Conference:
Austin Texas January 24 - 26, 1983
ISBN:
978-0-89791-090-3
Published:
24 January 1983
Sponsors:
Next Conference
January 19 - 25, 2025
Denver , CO , USA
Bibliometrics
Skip Abstract Section
Abstract

The papers in this volume were presented at the Tenth Annual ACM Symposium on the Principals of Programming Languages, sponsored jointly by SIGACT and SIGPLAN. They were selected from 170 abstracts submitted in response to the program committee's call for papers.

Skip Table Of Content Section
Article
Free
Five paradigm shifts in programming language design and their realization in Viron, a dataflow programming environment

We describe five paradigm shifts in programming language design, some old and some relatively new, namely Effect to Entity, Serial to Parallel, Partition Types to Predicate Types, Computable to Definable, and Syntactic Consistency to Semantic ...

Article
Free
Uncovering principles of novice programming

It is widely known that programming, even at a simple level, is a difficult activity to learn. Why is this so? Are novice difficulties really inherent in programming or are they related, to the nature of the programming tools currently given to novices? ...

Article
Free
Code generation for silicon

Compiler writers facea bleak future---soon everyone will be using Ada on the Nebula Architecture and there will be no further need for our services. Luckily, it appears to be possible to recycle compiler writers by encouraging them to build circuit ...

Article
Free
Derivation of efficient DAG marking algorithms

The best known linear-time list marking algorithms also require a linear amount of workspace. Algorithms working in bounded workspace have been obtained only by allowing quadratic execution time or by restricting the list structures to trees. We improve ...

Article
Free
Reasoning about nonatomic operations

A method is presented that permits assertional reasoning about a concurrent program even though the atomicity of the elementary operations is left unspecified. It is based upon a generalization of the dynamic logic operator [α]. The method is ...

Article
Free
Verifying reachability invariants of linked structures

The paper introduces a reachability predicate for linear lists, develops the elementary axiomatic theory of the predicate, and illustrates its application to program verification with a formal proof of correctness for a short program that traverses and ...

Article
Free
Practical program verification: automatic program proving for real-time embedded software

Despite the attractiveness of the concept, attempts to date to use proof of correctness techniques on production software have been generally unsuccessful. The obstacles encountered are not fundamental. We have implemented a proof of correctness system ...

Article
Free
Making variables abstract: an equational theory for Russell

One of the fundamental notions of programming, and thus of programming languages, is the variable. Recently, the variable has come under attack. The proponents of "functional programming" have argued that variables are at the root of all our problems in ...

Article
Free
Transformational programming: applications to algorithms and systems

Ten years ago Cheatham and Wegbreit [4] proposed a transformational program development methodology based on notions of top-down stepwise program refinement first expressed by Dijkstra [10] and Wirth [45]. A schema describing the process of this methodology ...

Article
Free
Polymorphic type inference

The benefits of strong typing to disciplined programming, to compile-time error detection and to program verification are well known. Strong typing is especially natural for functional (applicative) languages, in which function application is the central ...

Article
Free
Computer experiments with the REVE term rewriting system generator

A term rewriting system generator called REVE is described. REVE builds confluent and uniformly terminating term rewriting systems from sets of equations. Particular emphasis is placed on mechanization of termination proof. Indeed, REVE is one of the ...

Article
Free
Precise typing of abstract data type specifications

There are two important notions of data types being used in programming languages today. In the concept called abstract data types, types are algebras; the semantics of programs is described in terms of operations in these algebras. Another notion of ...

Article
Free
Automatic verification of finite state concurrent system using temporal logic specifications: a practical approach

We give an efficient procedure for verifying that a finite state concurrent system meets a specification expressed in a (propositional) branching-time temporal logic. Our algorithm has complexity linear in both the size of the specification and the size ...

Article
Free
"Sometimes" and "not never" revisited: on branching versus linear time (preliminary report)

Temporal logic ([PR57], [PR67]) provides a formalism for describing the occurrence of events in time which is suitable for reasoning about concurrent programs (cf. [PN77]). In defining temporal logic, there are two possible views regarding the underlying ...

Article
Free
How to cook a temporal proof system for your pet language

An abstract temporal proof system is presented whose program-dependent part has a high-level interface with the programming language actually studied. Given a new language, it is sufficient to deline the interface notions of atomic transitions, justice, ...

Article
Free
Structural semantics for polymorphic data types (preliminary report)

The semantic modeling of data types has been the subject of increased interest over the last few years, enhanced by the development of applicative languages such as Edinburgh's ML and HOPE, by the need for flexible highly structured languages that would ...

Article
Free
Incremental data flow analysis

In this paper we present ACINCF and ACINCB, incremental update algorithms for forward and backward data flow problems, which are based on a linear equations model of Allen/Cocke interval analysis [Allen 77, Ryder 82a]. We have studied their performance ...

Article
Free
Conversion of control dependence to data dependence

Program analysis methods, especially those which support automatic vectorization, are based on the concept of interstatement dependence where a dependence holds between two statements when one of the statements computes values needed by the other. ...

Article
Free
Loops in combinator-based compilers

In our paper [Wand 82a], we introduced a paradigm for compilation based on combinators. A program from a source language is translated (via a semantic definition) to trees of combinators; the tree is simplified (via associative and distributive laws) to ...

Article
Free
Compilation of data-driven programs for synchronous execution

We present algorithms that convert a class of parallel programs, called loop programs, from data-driven mode to synchronous mode. Such algorithms enable programmers to use a high-level, data-driven programming language without forfeiting the efficiency ...

Article
Free
Summarizing graphs by regular expressions

This paper shows how to rapidly determine the path relationships between k different elements of a graph (of the type primarily resulting from programs) in time proportional to k log k. Given the path relations between elements u,v, and w, it is easy to ...

Article
Free
A program form based on data dependency in predicate regions

A new program representation is presented which permits certain optimizations to be performed at less expense than with other forms. This paper describes code motion, common subexpression elimination and induction variable detection. Scalar propagation ...

Article
Free
Practical use of a polymorphic applicative language

Assembling a large system from its component elements is not a simple task. An adequate notation for specifying this task must reflect the system structure, accommodate many configurations of the system and many versions as it develops, and be a ...

Article
Free
On the unification of data and program abstraction in Ada

Ada is rich in the variety of its abstraction mechanisms. It has both a data abstraction mechanism (packages with private data types) that supports a functional programming style and a program abstraction mechanism (generic program units) that supports ...

Article
Free
Incremental polymorphic type checking in B

The programming language B has been designed for personal computing. In B, variables need not be declared, nor formal parameters specified. Nevertheless, B is strongly typed. All type requirements can be checked statically. To signal type violations on ...

Article
Free
Mechanisms for compile-time enforcement of security

This paper discusses features of a secure systems programming language designed and implemented at IBM's Watson Research Lab. Two features of the language design were instrumental in permitting security to be enforced with minimum run-time cost: (1) ...

Article
Free
Abstraction mechanisms in the BETA programming language

The BETA programming language is developed as part of the BETA project. The purpose of this project is to develop concepts, constructs and tools in the field of programming and programming languages. BETA has been developed from 1975 on and the various ...

Article
Free
Locality in software systems

This paper proposes a technique for what we call localization of power in computer systems, which can be viewed as a generalization of such linguistic disciplines as scope rules, strong typing and data-abstraction. Although the proposed technique is ...

Contributors
  • Association for Computing Machinery
  • University of Wisconsin-Madison
  • Cornell University
  • GrammaTech, Inc

Recommendations

Acceptance Rates

POPL '83 Paper Acceptance Rate28of170submissions,16%Overall Acceptance Rate824of4,130submissions,20%
YearSubmittedAcceptedRate
POPL '152275223%
POPL '142205123%
POPL '041762916%
POPL '031262419%
POPL '021282822%
POPL '011262419%
POPL '001513020%
POPL '991362418%
POPL '981753218%
POPL '972253616%
POPL '961483423%
POPL '941733923%
POPL '931993920%
POPL '922043015%
POPL '911523120%
POPL '891913016%
POPL '881772816%
POPL '871082927%
POPL '831702816%
POPL '821213831%
POPL '811212420%
POPL '791462718%
POPL '781352720%
POPL '771052524%
POPL '76902022%
POPL '751002323%
POPL '731002222%
Overall4,13082420%