A New Proof Rule for Almost-Sure Termination in Probabilistic Programming

Watch a 27-minute conference presentation from POPL 2018 exploring an innovative proof rule for demonstrating almost-sure termination in probabilistic programs. Dive into the research by Annabelle McIver, Carroll Morgan, Benjamin Lucien Kaminski, and Joost-Pieter Katoen as they introduce a novel method that directly analyzes source code, even for programs containing demonic non-determinism. Learn about their groundbreaking approach using variant functions (super-martingales) with parametric decreases in both amount and probability, understanding how this advancement extends beyond existing rules and connects to classical denumerable Markov chain results. Gain insights into proving zero probability mass for diverging runs in probabilistic programming through this technical presentation delivered at the prestigious ACM SIGPLAN conference.