Types and trace effects of higher order programs

Abstract

This paper shows how type effect systems can be combined with model-checking techniques to produce powerful, automatically verifiable program logics for higher order programs. The properties verified are based on the ordered sequence of events that occur during program execution, so-called event traces. Our type and effect systems infer conservative approximations of the event traces arising at run-time, and model-checking techniques are used to verify logical properties of these histories. Our language model is based on the -calculus. Technical results include a type inference algorithm for a polymorphic type effect system, and a method for applying known model-checking techniques to the trace effects inferred by the type inference algorithm, allowing static enforcement of history- and stack-based security mechanisms. A type safety result is proven for both unification and subtyping constraint versions of the type system, ensuring that statically well-typed programs do not contain trace event checks that can fail at run-time. © 2007 Cambridge University Press.