Cost-based analysis of probabilistic programs mechanised in HOL
Orieta Celiku, Annabelle K. McIver · Nordic journal of computing · 2004
We provide a HOL formalisation for analysing expected time bounds for probabilistic programs. Our formalisation is based on the quantitative program logic of Morgan et al. [21] and McIver's extension of it [17] to include performance-style operators. In addition we provide some novel results based on probabilistic data refinement which we use to improve the utility of the basic method.