λ-calculus and Quantitative Program Analysis
Chris Hankin, Herbert Wiklicky · Electronic Notes in Theoretical Computer Science · 2005
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.