To Zip Through the Cost Analysis of Probabilistic Programs

TL;DR

This paper introduces a refinement-typed probability monad in Liquid Haskell for automated reasoning about expected runtime of probabilistic programs, extending to infinite distributions and verified through case studies.

Contribution

It presents a novel refinement-typed probability monad in Liquid Haskell that enables automated expected runtime analysis of probabilistic programs, including infinite distributions.

Findings

Automated reasoning with minimal annotations for meldable heaps and coupon collector.

First formal verification of expected runtime for zip trees.

Framework effectively integrates with interactive proofs for complex probabilistic algorithms.

Abstract

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.