λ-calculus and Quantitative Program Analysis

In this paper we show how the framework of probabilistic abstract interpretation can be applied to statically analyse a probabilistic λ-calculus. We start by reviewing the classical framework of abstract interpretation. We choose to use (first-order) strictness analysis as our running example. We present the definition of probabilistic abstract interpretation and use it to construct a probabilistic strictness analysis.