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 8 Issue 2, April 1986

Toward compiler implementation correctness proofs
Laurian M. Chirica, David F. Martin
Pages: 185-214
DOI: 10.1145/5397.30847
Aspect of the interaction between compiler theory and practice is addressed. Presented is a technique for the syntax-directed specification of compilers together with a method for proving the correctness of their parse-driven implementations....

The ML approach to the readable all-purpose language
C. R. Spooner
Pages: 215-243
DOI: 10.1145/5397.5918
The ideal computer language is seen as one that would be as readable as natural language, and so adaptable that it could serve as the only language a user need ever know. An approach to language design has emerged that shows promise of allowing...

Automatic verification of finite-state concurrent systems using temporal logic specifications
E. M. Clarke, E. A. Emerson, A. P. Sistla
Pages: 244-263
DOI: 10.1145/5397.5399
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...

A short proof of a conjecture of De Remer and Pennello
Thomas J. Sager
Pages: 264-271
DOI: 10.1145/5397.30850
In this paper we offer a short proof of the DeRemer-Pennello conjecture that if the LR(0) automaton for a grammar G contains a state p and a nonterminal A such that (p,...