Semantic Logical Relations for Timed Message-Passing Protocols

on YouTube ↗19m

" summary

Presents a semantic logical relation that proves any well‑typed program inhabits the timed protocol relation (fundamental theorem) and also lets per‑instance verify foreign code, with a Rust type checker that uses an SMT solver to discharge timing constraints. Demonstrates on a smart‑home sensor case where communications require concrete gaps like 30 ms warmup and 20 ms cooldown, models time as natural numbers, ships evaluated artifacts, and reports the SMT‑based checking works surprisingly well.

AI-written summary · about

" chapters (15)

1. 0:00Timed message-passing protocols
2. 1:11Timing constraints matter
3. 2:35Process calculus for timed systems
4. 3:28Logical relations for verification
5. 4:31Intuitionistic linear logic session types
6. 6:38Timing constraints in session types
7. 7:40Operational semantics with timed transitions
8. 9:03Timed synchronization dynamics
9. 9:24Logical relations for behavioral typing
10. 10:06Latent versus urgent interpretations
11. 11:31Urgent interpretation for choices
12. 12:15Future-proof guarantees
13. 14:19Related work and context
14. 15:01Conclusion and future research
15. 16:25Q&A on real-time and logic