Effects and Coeffects in Call-By-Push-Value

on YouTube ↗19m

" summary

Presents a type system for call-by-push-value that statically bounds both observable effects and environmental demands and proves effect-and-coeffect soundness for two runtime models: a generic semantics and a resource-aware semantics that discards unused pure work but always runs effectful code. Translations from source examples into CBPV preserve effects and coeffects, dead‑code elimination for pure unused computations is validated, and all results are fully Coq mechanization with reusable artifacts and reproduced experiments.

AI-written summary · about

" chapters (13)

1. 0:00Effects and coeffects intro
2. 0:23Dead code elimination example
3. 1:45Effects in type systems
4. 2:46Coeffects on inputs
5. 4:36Call-by-push-value overview
6. 6:23Splitting expressions
7. 8:09Translating programs to call-by-push-value
8. 10:36Annotating call-by-push-value with effects and coeffects
9. 11:59Semantics of computations
10. 13:02Separating effects and coeffects
11. 13:43Summary and future work
12. 14:04Q&A: equational theory
13. 17:55Q&A: practical apps