This book covers various programming languages for probabilistic programming. The languages are described using syntax, semantics, and examples. It also looks at the theories related to the semantics of probability constructs and discusses the reasoning behind such programs. The preface divides the book into five parts: semantics (chapters 1 through 4), verification (chapters 5 through 8), logic (chapters 9 and 10), security (chapters 11 and 12), and programming languages (chapters 13 through 15).
Chapter 1 defines a simple imperative language with a random number generator in the interval [0,1], and another generating zero or one. The definition consists of syntax, operational semantics, and denotational semantics. Measure theory is used to express equations of semantics. Chapter 2 defines a language with types, sample, score, and normalize. The sample can be used for sampling data, the score can be used for observations, and normalize can be used with inference algorithms for calculating posteriors. The chapter gives semantics based on s-finite kernels over measurable spaces. Chapter 3 first discusses how a computable distribution library can be built for continuous distributions. It defines a typed language with dist (dist is used for distributions). The semantics of the language are given using topological domains. Chapter 4 introduces the lambda calculus for probabilistic programming. It observes two variants, the randomized lambda calculus and the Bayesian lambda calculus, and gives simple language for each of them.
Chapter 5 is on a proof technique called proof by coupling. It begins by introducing coupling in the distributions. The technique consists of a language, logical rules, and the construction of such proofs. The chapter ends with related works. Chapter 6 is on reasoning about the expected runtime of a probabilistic program. It gives formal computational rules for a defined language and discusses the challenges to defining such rules. Chapter 7 discusses bounded termination for probabilistic programs. A language with probabilities, the foundation details of bounded termination, and proof techniques are discussed. Chapter 8 is on reasoning about variables in the programs. The static analysis with variable symbols is supported by what is referred to as concentration in measure inequalities (CMI). The chapter provides a primer on CMI, as well as how to apply reasoning on probabilistic variables.
Chapter 9 introduces a reasoning framework using channels and associated Bayesian inference. The semantics given by state/predicate transformations are recognized as channels. The networks and categories formed are applied to Bayesian network inference techniques to reason about the probabilistic programs. Chapter 10 presents a reasoning framework for quantitative analysis. The framework uses equations, which form metrics. A background in equation logistics with respect to probabilistic programs is included.
Chapter 11 is on a privacy monitor for a system. Individuals have privacy data, which can be queried online. Data access is allowed, but should still detect if queries derive any private information. The monitor can use Bayesian methods to develop bounds for query access. Abstract interpretation is used for developing such monitors. Chapter 12 presents a language called Knife. Knife has explicit distributions. It is embedded inside Haskell. The application shows quantitative information flow security.
Chapter 13 describes the Luck testing language. Matching semantics are given for Luck after the syntax. Implementation details include a pattern matching compiler developed using the matching semantics. Chapter 14 presents an extension of the language called Tabular. Tabular is a language for relational databases implemented on spreadsheets. The extension is for probabilistic programming, and reductions from extended Tabular to core Tabular are described. Chapter 15 looks at the reliability analysis of approximations in the programs/hardware. It gives reliability specifications and discusses related things.
The book can be used in a PhD-level course, as it requires knowledge of the theory of programming languages, the theory of probability, measure theory, and for some chapters, category theory, databases, reasoning, and so on. In order to use the book in practice, experience is required in all these areas. That being said, the book is not only theoretical; it also includes many examples for understanding. Applications are offered in security, databases, testing, and reasoning about program quantities.