Program logics à la carte

on YouTube ↗21m

" summary

Combines reusable program-logic fragments for language effects (shared state, concurrency, nondeterminism) so logics can be composed rather than rebuilt. Uses Interaction Trees (ITrees) to express semantics, Iris for separation logic, and a mechanized Coq development to prove soundness and provide reusable artifacts.

AI-written summary · about

" chapters (8)

1. 0:00Introduction
2. 2:50Reusable program logics
3. 5:39iTree logic
4. 8:08Custom logic recipe
5. 10:13Demo: lambda calculus & heap effects
6. 13:01Abstraction benefits
7. 14:43Advanced features & case studies
8. 16:11Q&A