Algebraic Temporal Effects: Temporal Verification of Recursively Typed Higher-Order(…)

on YouTube ↗21m

" summary

Proposes algebraic temporal effects: an axiomatized effect algebra plus an R modality for guarded recursive types that stratifies infinite behavior, an effect system, and mechanized proofs of safety and liveness soundness. Uses guarded recursion with a later-like constructor, an R operation to accumulate finite trace chunks and a fin operation to compute an upper bound; shows two concrete instances: temporal regular effects (ω-regular expressions) and temporal fixpoint effects (first-order fixpoint logic). Demonstrations include recursive, concurrent and object‑oriented examples and the system rejects cases where nontermination breaks file-close liveness.

AI-written summary · about

" chapters (10)

1. 0:00Temporal verification intro
2. 1:07Safety vs liveness in temporal verification
3. 3:17Current temporal effect limits
4. 4:40Temporal effects with recursive types
5. 6:06Temporal effect systems background
6. 10:27Recursive structure challenges
7. 11:53Guarded recursion and R modalities
8. 13:17Infinite behavior with guarded recursion
9. 16:14Algebraic temporal effects
10. 18:23Summary and conclusion