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 - an event history. Our type and effect systems automatically infer conservative approximations of the event histories arising at runtime, 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 powerful type inference algorithm for a polymorphic type effect system, and a method for applying known model-checking techniques to the history effects inferred by the type inference algorithm, allowing static enforcement of history- and stack-based security mechanisms.
Skalka, C., & Smith, S. (2004). History effects and verification. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 3302, 107–128. https://doi.org/10.1007/978-3-540-30477-7_8