Probabilistic programming and the formal analysis of probabilistic algorithms are active areas of research, driven by the widespread use of randomness to improve performance. While functional correctness has seen substantial progress, automated reasoning about expected runtime remains comparatively limited. In this work, we address this challenge by introducing a refinement-typed probability monad in Liquid Haskell. Our monad enables automated reasoning about expected values and costs by encoding probabilistic behaviour directly in types. Initially defined for discrete distributions over finite support, it is extended to support infinite distributions via an axiomatic approach. By leveraging Liquid Haskell's SMT-based refinement type checking, our framework provides a high degree of automation. We evaluate our approach through four case studies: meldable heaps, coupon collector, randomised quicksort, and zip trees. The first two demonstrate automation with minimal annotation overhead. The latter two showcase how our monad integrates with interactive proofs, including the first formal verification of the expected runtime of zip trees.

翻译：概率编程与概率算法的形式化分析是当前活跃的研究领域，其驱动力在于随机性被广泛用于提升算法性能。虽然功能正确性分析已取得显著进展，但关于期望运行时间的自动化推理仍然相对有限。本研究通过引入基于Liquid Haskell的细化类型概率单子来解决这一挑战。该单子通过将概率行为直接编码在类型系统中，实现了对期望值与计算成本的自动化推理。该框架最初针对有限支撑上的离散分布定义，后通过公理化方法扩展至支持无限分布。借助Liquid Haskell基于SMT的细化类型检查机制，本框架提供了高度自动化的验证能力。我们通过四个案例研究评估了该方法：可合并堆、优惠券收集问题、随机快速排序以及zip树。前两个案例展示了仅需少量标注即可实现自动化验证；后两个案例则展现了该单子如何与交互式证明相结合，其中包含对zip树期望运行时间的首次形式化验证。