Probabilistic Lambda-calculus and Quantitative Program Analysis

We show how the framework of probabilistic abstract interpretation can be applied to statically analyse a probabilistic version of the {lambda}-calculus. The resulting analysis allows for a more speculative use of its outcomes based on the consideration of statistically defined quantities. After introducing a linear operator based semantics for our probabilistic {lambda}-calculus {Lambda}p, and reviewing the framework of abstract interpretation and strictness analysis, we demonstrate our technique by constructing a probabilistic (first-order) strictness analysis for {Lambda}p.