Journal of Functional Programming

Articles

Types and trace effects of higher order programs

CHRISTIAN SKALKAa1, SCOTT SMITHa2 and DAVID VAN HORNa3

a1 The University of Vermont, Burlington, Vermont, USA (email: skalka@cs.uvm.edu)

a2 The Johns Hopkins University, Baltimore, Maryland, USA (email: scott@cs.jhu.edu)

a3 Brandeis University, Waltham, Massachusetts, USA (email: dvanhorn@cs.brandeis.edu)

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.