Annotated reading list

This page contains a collection of interesting probabilistic programming papers organized by topic that are relevant to the course. This bibliography is not meant to be exhaustive of all useful papers; it is meant to contain a good starting point for each of the major topic areas. These papers are a mix of classic papers and papers that I want to read. Feel free to peruse these papers for project ideas. These papers are sorted chronologically within each category.

Another excellent resource is the following textbook:

Barthe, G., Katoen, J.-P., & Silva, A. (2020). Foundations of probabilistic programming. Cambridge University Press.

  1. Annotated reading list
  2. Semantics
  3. Probabilistic Verification
  4. Verified Inference
  5. Automatic Differentiation

Semantics

These papers are concerned with the question of “what does a probabilistic program mean”? Some of the earliest papers in probabilistic programming asked this question, and it remains a core topic of interest within probabilistic programming today. Today, much of the challenge within this area focuses on giving meaning to languages with rich features: higher-order functions, continuous random variables, and continuous conditioning.

Lawvere, F. W. (1962). The category of probabilistic mappings. Preprint. https://ncatlab.org/nlab/files/lawvereprobability1962.pdf A well-known unpublished note from Lawvere that initiated the study of categorical probability.
Kozen, D. (1979). Semantics of probabilistic programs. 20th Annual Symposium on Foundations of Computer Science (Sfcs 1979), 101–114. The first paper to formalize the notion of a probabilistic program.
Giry, M. (1986). A categorical approach to probability theory. In Categorical Aspects of Topology and Analysis. https://doi.org/10.1007/BFb0092872 Introduced the "Giry monad"
Ramsey, N., & Pfeffer, A. (2002). Stochastic Lambda Calculus and Monads of Probability Distributions. Proceedings of the 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 154–165. https://doi.org/10.1145/503272.503288 Develops a core probabilistic programming calculus using the probability monad. A good first read.
Heunen, C., Kammar, O., Staton, S., & Yang, H. (2017). A Convenient Category for Higher-Order Probability Theory. Proceedings of the 32nd Annual ACM/IEEE Symposium on Logic in Computer Science. Introduced the quasi-Borel space as a categorical foundation for higher-order continuous PPLs
Narayanan, P., & Shan, C.-chieh. (2020). Symbolic Disintegration with a Variety of Base Measures. ACM Trans. Program. Lang. Syst., 42(2). https://doi.org/10.1145/3374208 Develops Hakaru, a language that nicely handles conditioning in the continuous setting.

Probabilistic Verification

These papers are concerned with the question of verifying correctness properties of probabilistic programs and systems. Example of applications include verifying differential privacy and verifying the correctness of randomized algorithms.

Kozen, D. (1983). A probabilistic pdl. Proceedings of the Fifteenth Annual ACM Symposium on Theory of Computing, 291–297. https://www.cambridge.org/core/books/foundations-of-probabilistic-programming/ The first example of a program logic for probabilistic programs.
Morgan, C., McIver, A., & Seidel, K. (1996). Probabilistic predicate transformers. ACM Transactions on Programming Languages and Systems (TOPLAS), 18(3), 325–353. Introduced probabilistic predicate transformers and weakest pre-expectations.
Barthe, G., Gaboardi, M., Grégoire, B., Hsu, J., & Strub, P.-Y. (2016). Proving Differential Privacy via Probabilistic Couplings. Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, 749–758. https://doi.org/10.1145/2933575.2934554 One of the earlier papers on verifying probabilistic properties via coupling.
Vasilenko, E., Vazou, N., & Barthe, G. (2022). Safe Couplings: Coupled Refinement Types. Proc. ACM Program. Lang., 6(ICFP). https://doi.org/10.1145/3547643 An interesting application of refinement types to verifying properties of probabilistic programs.

Verified Inference

These papers are concerned with the question of “how do we determine whether or not a probabilistic programming system is correctly implemented”? It is notoriously difficult to implement inference algorithms correctly, and increasingly important decisions are being made based on the outcome of inference computations, making this a very important area for research in modern PPLs.

Automatic Differentiation

What does automatic differentiation have to do with probabilistic programs? It turns out the two are intimately related: automatic differentiation can inform how we explore the search space during probabilistic inference. This is critical for scaling inference on certain kinds probabilistic programs. Beyond inference, automatic differentiation has can facilitate other kinds of probabilistic programming tasks like maximum-likelihood learning.