Foundations of Probabilistic Programming

What does a probabilistic program mean, and how can its behavior be reasoned about with mathematical precision? Foundations of Probabilistic Programming brings together 15 chapters addressing these questions, from the semantics of probabilistic computation to verification, privacy, and practical programming languages. The result is a research-grounded collection for readers interested in the ideas beneath software that computes with uncertainty.

From program meaning to formal analysis

The chapters develop several complementary ways to understand probabilistic programs. Topics include probability measures and computable distributions, probabilistic lambda calculi, program logics, and quantitative equational reasoning. Together, these approaches help frame the central challenge of the field: describing not only what a program can do, but how likely its different outcomes are.

Reasoning about runtime, termination, and risk

Formal analysis takes practical questions seriously. Contributions examine expected runtime, termination using martingales, concentration inequalities, and probabilistic abstract interpretation. Other chapters connect probability with security and privacy, including ways to reason about how information may flow from a program’s internal state to an observer.

Applications beyond theory

The collection also explores Bayesian reasoning and quantitative information flow, including an account using monads in Haskell. Its application-focused chapters introduce probabilistic programming through testing, spreadsheet-based inference, and programming for unreliable hardware. These examples show the range of settings in which probabilistic models and program analysis meet.

Who will find it useful?

Edited by Gilles Barthe, Joost-Pieter Katoen, and Alexandra Silva, this volume is aimed at graduate students and readers from neighboring areas of computer science who want a structured introduction to the field’s theoretical underpinnings. Its breadth makes it relevant to interests in programming languages, formal verification, machine learning, statistics, and computer security.

A substantial, open-access reference

Rather than focusing on one probabilistic language or technique, the book assembles distinct perspectives into a broad view of the discipline. The publisher identifies its digital edition as open access under a Creative Commons Attribution license. 📚