Print

Van Horn, David

Computer Science

2006

MS

Trace effect analysis empowers programmers to make assertions on the temporal sequence of atomic program events having occurred at any point in the computation of a program. A polymorphic type and effect inference system automatically extracts an abstract interpretation conservatively approximating the events and assertions that will arise at run-time. Such an interpretation can then be model-checked to obtain a static verification of these temporal program logics for higher-order programs of a [lambda]-calculus extended with notions of atomic events, temporal assertions, and computational traces. The purpose of this thesis is to demonstrate that trace effect analysis is implementable and to prove the implementation sound with respect to its logical specification. This thesis describes both the logical and algorithmic type and effect system and applications of the analysis to the static enforcement of security mechanisms. The systems use an effectual weakening rule, and enjoy a unified representation of types resulting in concise specifications of programs. A type inference algorithm is presented and an algorithmic soundness result is established with respect to its logical counterpart. An implementations of the inference algorithm is provided. Finally, extensions to the system are defined, discussed, and implemented.