Property-based random testing á la QuickCheck requires building efficient generators for well-distributed random data satisfying complex logical predicates, but writing these generators can be difficult and error prone. This chapter introduces a probabilistic domain-specific language in which generators are conveniently expressed by decorating predicates with lightweight annotations to control both the distribution of generated values and the amount of constraint solving that happens before each variable is instantiated. This language, called Luck, makes generators easier to write, read and maintain. We give Luck a probabilistic formal semantics and prove several fundamental properties, including the soundness and completeness of random generation with respect to a standard predicate semantics. We evaluate Luck on common examples from the property-based testing literature and on two significant case studies, showing that it can be used in complex domains with comparable bug-finding effectiveness and a significant reduction in testing code size compared to handwritten generators.

In this chapter, we explore how (Type-2) computable distributions can be used to give both (algorithmic) sampling and distributional semantics to probabilistic programs with continuous distributions. To this end, we sketch an encoding of computable distributions in a fragment of Haskell and show how topological domains can be used to model the resulting PCF-like language. We also examine the implications that a (Type-2) computable semantics has for implementing conditioning. We hope to draw out the connection between an approach based on (Type-2) computability and ordinary programming throughout the chapter as well as highlight the relation with constructive mathematics (via realizability).

This chapter is concerned with analysing the expected runtime of probabilistic programs by exploiting program verification techniques. We introduce a weakest pre-conditioning framework á la Dijkstra that enables to determine the expected runtime in a compositional manner. Like weakest pre-conditions, it is a reasoning framework at the syntax level of programs. Applications of the weakest pre-conditioning framework include determining the expected runtime of randomised algorithms, as well as determining whether a program is positive almost-surely terminating, i.e., whether the expected number of computation steps until termination is finite for every possible input. For Bayesian networks, a restricted class of probabilistic programs, we show that the expected runtime analysis can be fully automated. In this way, the simulation time under rejection sampling can be determined. This is particularly useful for ill-conditioned inference queries.

Monads are a popular feature of the programming language Haskell because they can model many different notions of computation in a uniform and purely functional way. Our particular interest here is the probability monad, which can be -- and has been -- used to synthesise models for probabilistic programming. Quantitative Information Flow, or QIF, arises when security is combined with probability, and concerns the measurement of the amount of information that 'leaks' from a probabilistic program's state to a (usually) hostile observer: that is, not 'whether' leaks occur but rather 'how much?' Recently it has been shown that QIF can be seen monadically, a 'lifting' of the probability monad so that programs become functions from distributions to distributions of distributions: the codomain is 'hyper distributions'. Haskell's support for monads therefore suggests a synthesis of an executable model for QIF. Here, we provide the first systematic and thorough account of doing that: using distributions of distributions to synthesise a model for Quantitative Information Flow in terms of monads in Haskell.

Tabular is a domain-specific language for expressing probabilistic models of relational data. Tabular has several features that set it apart from other probabilistic programming languages including: (1) programs and data are stored as spreadsheet tables; (2) programs consist of probabilistic annotations on the relational schema of the data; and (3) inference returns estimations of missing values and latent columns, as well as parameters. Our primary implementation is for Microsoft Excel and relies on Infer.NET for inference. Still, the language can be called independently of Excel and can target alternative inference engines.

Equational logic has been a central theme in mathematical reasoning and in reasoning about programs. We introduce a quantitative analogue of equational reasoning that allows one to reason about approximate equality. The equality symbol is annotated with a real number that describes how far apart two terms can be. We develop the counterparts of standard results of equational logic, in particular, a completeness theorem. We define quantitative algebras and free quantitative algebras which yield monads on categories of metric spaces. We show that key examples of probability metrics, in particular, the Kantorovich metric and the Wasserstein p-metrics, arise from simple quantitative theories. Finally we develop a quantitative version of the theory of effects in programming languages.

Probabilistic couplings are a powerful abstraction for analysing probabilistic properties. Originating from research in probability theory, a coupling is a distribution over pairs that relates – or couples – two given distributions. If we can find a coupling with certain properties, then we can conclude properties about the two related distributions. In this way, probabilistic relational properties – properties comparing two executions of a probabilistic program – can be established by building a suitable coupling. Couplings have also been explored in the logic and verification literature. For example, probabilistic bisimulation asserts that there exists a coupling; in this way, couplings can be used to verify equivalence of finite state probabilistic transition systems. However, their use in mathematics suggests that couplings can prove more sophisticated properties for richer probabilistic computations, such as imperative programs and infinite state systems. Furthermore, we can borrow a tool from probability theory, called proof by coupling, to construct couplings in a compositional fashion. This chapter describes how coupling proofs can be naturally encoded in pRHL, a relational program logic originally designed for verifying cryptographic protocols. Several examples are presented, showing how to use this proof technique to verify equivalence, stochastic domination and probabilistic convergence.

For non-probabilistic programs, a key question in static analysis is termination, which asks whether a given program terminates under a given initial condition. In the presence of probabilistic behaviour, there are two fundamental extensions of the termination question: (a) the almost-sure termination question, which asks whether the termination probability is 1; and (b) the bounded-time termination question, which asks whether the expected termination time is bounded. There are many active research directions to address these two questions; one important such direction is the use of martingale theory for termination analysis. In this chapter, we survey the main techniques of the martingale-based approach to the termination analysis of probabilistic programs.

Bayesian probability models uncertain knowledge and learning from observations. As a defining feature of optimal adversarial behaviour, Bayesian reasoning forms the basis of safety properties in contexts such as privacy and fairness. Probabilistic programming is a convenient implementation of Bayesian reasoning but the adversarial setting imposes obstacles to its use: approximate inference can underestimate adversary knowledge and exact inference is impractical in cases covering large state spaces. By abstracting distributions, the semantics of a probabilistic language, and inference, jointly termed probabilistic abstract interpretation, we demonstrate adversary models both approximate and sound. We apply the techniques to build a privacy-protecting monitor and describe how to trade off the precision and computational cost in its implementation while remaining sound with respect to privacy risk bounds.

This chapter offers an accessible introduction to the channel-based approach to Bayesian probability theory. This framework rests on algebraic and logical foundations, inspired by the methodologies of programming language semantics. It offers a uniform, structured and expressive language for describing Bayesian phenomena in terms of familiar programming concepts, like channel, predicate transformation and state transformation. The introduction also covers inference in Bayesian networks, which will be modelled by a suitable calculus of string diagrams.