Recalling a Witness - Foundations and Applications of Monotonic State

Watch a 24-minute conference talk from POPL 2018 exploring a novel approach to program verification through monotonic state reasoning. Learn how to simplify verification of programs with evolving states by leveraging the monotonic-state monad, a compact interface for Hoare-style reasoning in dependently typed languages. Discover how properties witnessed in prior states can be recalled in current states when state evolution follows specific preorders, eliminating the need for explicit program invariants. Follow along as the speakers demonstrate the practical applications of this approach through F* verification system examples and implementations in distributed systems. Gain insights into program verification techniques including Hoare logic, modular reasoning, monotonic references, and formal foundations for secure file transfer and state continuity.