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 23 Issue 5, September 2001

Operator strength reduction
Keith D. Cooper, L. Taylor Simpson, Christopher A. Vick
Pages: 603-625
DOI: 10.1145/504709.504710
Operator strength reduction is a technique that improves compiler-generated code by reformulating certain costly computations in terms of less expensive ones. A common case arises in array addressing expressions used in loops. The compiler can...

Mechanizing a theory of program composition for UNITY
Lawrence C. Paulson
Pages: 626-656
DOI: 10.1145/504709.504711
Compositional reasoning must be better understood if non-trivial concurrent programs are to be verified. Chandy and Sanders [2000] have proposed a new approach to reasoning about composition, which Charpentier and Chandy [1999] have illustrated by...

An indexed model of recursive types for foundational proof-carrying code
Andrew W. Appel, David McAllester
Pages: 657-683
DOI: 10.1145/504709.504712
The proofs of "traditional" proof carrying code (PCC) are type-specialized in the sense that they require axioms about a specific type system. In contrast, the proofs of foundational PCC explicitly define all required types and explicitly prove all...