Algebraic Temporal Effects: Temporal Verification of Recursively Typed Higher-Order Programs

Watch this 21-minute conference talk from POPL 2025 where researchers Taro Sekiyama and Hiroshi Unno present their work on algebraic temporal effects for verifying temporal properties in higher-order programs with recursive types. Learn how they address the challenge of unstructured loops in recursive types by introducing temporal effects with a later modality, which stratifies loops to capture non-terminating program behavior. The presentation explains their abstract, algebraic approach to temporal effects that clarifies requirements for sound program reasoning, along with two practical implementations: temporal regular effects based on ω-regular expressions and temporal fixpoint effects based on first-order fixpoint logic. See demonstrations of these concepts applied to concurrent and object-oriented programming examples. This research contributes to the field of temporal verification by extending effect systems to handle recursively typed higher-order programs while maintaining both safety and liveness soundness.