enter search term and/or author name
Operator strength reduction
Keith D. Cooper, L. Taylor Simpson, Christopher A. Vick
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
Compositional reasoning must be better understood if non-trivial concurrent programs are to be verified. Chandy and Sanders  have proposed a new approach to reasoning about composition, which Charpentier and Chandy  have illustrated by...
An indexed model of recursive types for foundational proof-carrying code
Andrew W. Appel, David McAllester
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...