A Modal Deconstruction of Löb Induction

This conference talk from POPL 2025 presents Daniel Gratzer's research on a novel analysis of the Löb induction principle from guarded recursion. Explore how the researcher leverages recent advances in modal type theory and univalent foundations to derive Löb induction from simpler, more conceptual primitives. Learn about Gatsby, the first guarded type theory that captures the rich modal structure of the topos of trees alongside Löb induction without immediately precluding canonicity or normalization. Discover how Gatsby can recover many prior approaches to guarded recursion while using its additional power to improve on previous examples. The presentation demonstrates a new application of univalent foundations to programming language theory, relying on crucial homotopical insights. The 18-minute talk was presented at the ACM SIGPLAN POPL 2025 conference, with the full research article available through DOI: 10.1145/3704866.