λ-calculus and Quantitative Program Analysis (Extended Abstract)

AbstractIn 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