ACM DL

Programming Languages and Systems (TOPLAS)

Menu

Search Issue
enter search term and/or author name

Archive


ACM Transactions on Programming Languages and Systems (TOPLAS) - The MIT Press scientific computation series, Volume 8 Issue 3, July 1986

Smart recompilation
Walter F. Tichy
Pages: 273-291
DOI: 10.1145/5956.5959
With current compiler technology, changing a single line in a large software system may trigger massive recompilations. If the change occurs in a file with shared declarations, all compilation units depending upon that file must be recompiled to...

The concept of a supercompiler
Valentin F. Turchin
Pages: 292-325
DOI: 10.1145/5956.5957
A supercompiler is a program transformer of a certain type. It traces the possible generalized histories of computation by the original program, and compiles an equivalent program, reducing in the process the redundancy that could be present in...

An example of stepwise refinement of distributed programs: quiescence detection
Mani Chandy, Jayadev Misra
Pages: 326-343
DOI: 10.1145/5956.5958
We propose a methodology for the development of concurrent programs and apply it to an important class of problems: quiescence detection. The methodology is based on a novel view of programs. A key feature of the methodology is the separation of...

Proving systolic systems correct
Matthew Hennessy
Pages: 344-387
DOI: 10.1145/5956.5999

A language for describing communicating systems is described. It is sufficiently expressive to describe both the desired behavior of systems, their specifications, and their actual implementations in terms of simpler components. We...

Correctness proofs of distributed termination algorithms
Krzysztof R. Apt
Pages: 388-405
DOI: 10.1145/5956.6000
The problem of correctness of the solutions to the distributed termination problem of Francez [7] is addressed. Correctness criteria are formalized in the customary framework for program correctness. A very simple proof method is proposed and...

Comments on Georgeff's “transformations and reduction strategies for typed lambda expressions”
Flemming Nielson, Hanne Rus Nielson
Pages: 406-407
DOI: 10.1145/5956.215007
In his recent paper, Georgeff [1] considers the evaluation of lambda expres sions (with reducing reflexive types) on a variant of Landin's SECD machine. It is observed that for so-called simple expressions the SECD machine will construct...