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), Volume 9 Issue 1, Jan. 1987

Writing Larch interface language specifications
Jeannette M. Wing
Pages: 1-24
DOI: 10.1145/9758.10500
Current research in specifications is emphasizing the practical use of formal specifications in program design. One way to encourage their use in practice is to provide specification languages that are accessible to both designers and...

The geometry of semaphore programs
Scott D. Carson, Paul F. Reynolds, Jr.
Pages: 25-53
DOI: 10.1145/9758.9759
Synchronization errors in concurrent programs are notoriously difficult to find and correct. Deadlock, partial deadlock, and unsafeness are conditions that constitute such errors. A model of concurrent semaphore programs based on...

On the algebraic definition of programming languages
Manfred Broy, Martin Wirsing, Peter Pepper
Pages: 54-99
DOI: 10.1145/9758.10501
The algebraic specification of the semantics of programming languages is outlined. Particular emphasis is given to the problem of specifying least-fixed points by first-order conditional equations. To cover this issue, the theory of specifying...

Soundness of Hoare's logic: an automated proof using LCF
Stefan Sokolowski
Pages: 100-121
DOI: 10.1145/9758.11326
This paper presents a natural deduction proof of Hoare's logic carried out by the Edinburgh LCF theorem prover. The emphasis is on the way Hoare's theory is presented to the LCF, which looks very much like an exposition of syntax and semantics...