Probabilistic Programming (Fall 2025)

Motivation

The idea behind this reading group is to become more familiar with some of the recent literature on semantics, verification and applications of probabilistic programming.

Schedule

  • When: TBD
  • Where: TBD
  • Organizer: Alejandro Aguirre

We will be holding the kick-off meeting on Tuesday, September 2nd at 9AM in the Turing 230 meeting room (together with the proof automation reading group), to discuss the format, the schedule, and the list of papers.

Format

We meet every other week, alternating with the proof automation reading group.

The concrete format is to be determined. The preliminary idea is that a discussion lead is assigned 2-3 related papers and presents them to the rest of the group. The format of the presentation is up to the discussion lead, some options are slides, whiteboard, live coding, etc. The rest of the group is assumed to have read the paper introductions, but not the body of the paper in detail.

Suggested papers

A selection of papers is listed below. The list is open to suggestions depending on the interests of the group participants

Semantics

  • Measurable cones and stable, measurable functions: a model for probabilistic higher-order programming. Ehrard et al. 2018. Link

  • A domain theory for statistical probabilistic programming. Vákár et al. 2019. Link

  • Semantics of higher-order probabilistic programs with conditioning. Dahlqvist and Kozen. 2020. Link

  • A Cartesian Closed Category for Random Variables. Di Gianantonio and Edalat. 2024. Link

  • The Beta-Bernoulli process and algebraic effects. Staton et al. 2018. Link

  • A synthetic approach to Markov kernels, conditional independence and theorems on sufficient statistics. Fritz. 2020. Link

  • Synthetic topology in Homotopy Type Theory for probabilistic programming. Bidlingmaier et al. 2021. Link

  • Other papers on categorical probability theory?

Logic and Verification

  • Towards Concurrent Quantitative Separation Logic. Fesefeldt et al. 2022. Link

  • A Quantitative Probabilistic Relational Hoare Logic. Avanzini et al. 2025. Link

  • Probabilistic Concurrent Reasoning in Outcome Logic: Independence, Conditioning, and Invariants. Zilberstein et al. 2024. Link

  • A Program Logic for Concurrent Randomized Programs in the Oblivious Adversary Model. Fan et al. 2025. Link

  • A Deductive Verification Infrastructure for Probabilistic Programs. Schröer et al. 2023. Link

  • Foundations for Deductive Verification of Continuous Probabilistic Programs: From Lebesgue to Riemann and Back. Batz et al. 2025. Link

  • Lilac: A Modal Separation Logic for Conditional Probability. Li et al. 2023. Link

  • Bluebell: An Alliance of Relational Lifting and Independence for Probabilistic Reasoning. Bao et al. 2025. Link

  • A Modal Type Theory of Expected Cost in Higher-Order Probabilistic Programs. Rajani et al. 2024. Link

  • Induction and Recursion Principles in a Higher-Order Quantitative Logic for Probability. Bacci and Møgelberg. 2024. Link

  • Lower Bounds for Possibly Divergent Probabilistic Programs. Feng et al. 2023. Link

  • Probabilistic Program Analysis with Martingales. Chakarov and Sankaranarayanan. 2013. Link

  • Sound and Complete Proof Rules for Probabilistic Termination. Majumdar and Sathiyanarayana. 2025. Link

  • Other papers on probabilistic separation logics

Statistical Inference

  • Scaling exact inference for discrete probabilistic programs. Holtzen et al. 2020. Link

  • Reactive Probabilistic Programming. Baudart et al. 2020. Link

Security and Privacy

  • Sound Verification of Security Protocols: From Design to Interoperable Implementations. Arquint et al. 2023. Link

  • EasyUC: Using EasyCrypt to Mechanize Proofs of Universally Composable Security. Canetti et al. 2019. Link

  • On Session Typing, Probabilistic Polynomial Time, and Cryptographic Experiments. Dal Lago and Giusti. 2022. Link

  • On Computational Indistinguishability and Logical Relations. Dal Lago et al. 2024. Link

  • Duet: an expressive higher-order language and linear type system for statically enforcing differential privacy. Near et al. 2019. Link

  • SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq. Abate et al. 2021. Link