A Separation Logic for Negative Dependence

on YouTube ↗18m

" summary

Design of LINA, a probabilistic separation logic that adds a second separating conjunction for negative dependence alongside the independence star, with semantics built from a nondeterministic composition operator. Introduces partition negative association (PNA) to make the NA-star compositional, proves closure under independent unions and monotone maps, and gives a Frame-like rule that preserves PNA when sampling a one‑hot vector and adding counts. Verifies balls‑into‑bins and bloom filter bounds and presents M‑BI as a sound complete BI extension.

AI-written summary · about

" chapters (7)

1. 0:00Intro
2. 0:20Motivating Example: Balls-into-Bins
3. 3:13Contribution
4. 4:11Separation Logic
5. 5:59Assertion Logic of LINA
6. 7:12Challenges: Semantics for
7. 11:52Program Logic of LINA

" related talks

• 01h 06mIntroduction to Causal Graphical Models: Graphs, d-separation, do-calculusSpencer Gordon · Causality Boot Camp
• 01h 00mLogic and Probabilistic Circuits 3YooJung Choi · Logic and Algorithms in Database Theory and AI Boot Camp
• 01h 03mLogic and Probabilistic Circuits 2YooJung Choi · Logic and Algorithms in Database Theory and AI Boot Camp
• 56mLog-concave Polynomials and Spectral Independence 3Kuikui Liu · Analysis and TCS Boot Camp 2023
• 54mNegative Dependence and Lorentzian PolynomialsPetter Brändén · Deterministic Counting, Probability, and Zeros of Partition Functions (Simons Institute workshop, 2019)
• 01h 01mBrief Tutorial on Probabilistic DatabasesDan Suciu · Uncertainty in Computation 2016
• 01h 02mOut-of-Distribution Generalization as Reasoning: Are LLMs Competitive?Les Valiant · Emerging Generalization Settings 2024
• 26mAffine Monads and Lazy Structures for Bayesian ProgrammingYounesse Kaddar, Sam Staton, Swaraj Dash, Hugo Paquet · POPL 2023