Diamonds Are Not Forever: Liveness in Reactive Programming with Guarded Recursion

on YouTube ↗29m

" summary

A new language called Lively RaTT combines guarded recursion with an inductive until type (e.g. diamond = unit until a) by treating the temporal circle modality as a submodality of the guarded triangle, preventing the inductive/coinductive collapse. The system uses a step-indexed Kripke logical relation with transfinite indexing to prove productivity, causality, termination of until-types, fairness for fair streams, and the absence of implicit space leaks; the operational semantics implements explicit heaps per time step.

AI-written summary · about

" chapters (11)

1. 0:00Intro
2. 4:43Lively RaTT, the first FRP language that combines the following properties
3. 8:34Diamonds are forever? We would like a type A expressing that a value of type A is available at some time in the future. For example, server: Request Response
4. 10:16Diamonds are not forever! Instead, we distinguish between two 'later modalities
5. 11:51Lively RaTT: An overview Properties of the language • No implicit space leaks
6. 13:15Later modalities, Fitch style In Lively RaTT
7. 17:59Until types We use the Until connective from linear temporal logic, to express temporal inductive types
8. 20:22Operational Semantics Operational semantics rules out implicit space leaks by construction
9. 22:50Step Semantics for streams For streams (types Str A)
10. 25:07Productivity and Causality We prove productivity and causality theorems: Theorem (Productivity)
11. 26:04Termination and Liveness We prove termination and liveness theorems. Theorem (Termination)