Decalf: A Directed, Effectful Cost-Aware Logical Framework

on YouTube ↗18m

" summary

Decalf is a directed, effectful, cost-aware logical framework implemented in Agda that equips every type with an intrinsic preorder so a cost bound can itself be a program; it adds a judgmental program inequality alongside a step primitive for abstract step-counting, supports algebraic effects (probabilistic choice, mutable state), and proves compositional bounds: insertion sort ≤ O(n^2) by inequality chains, merge sort ≤ n log n, randomized sublist yields a binomial cost distribution using an eraser lemma. Semantics are given in the topos of augmented simplicial sets; artifacts are mechanized and reusable.

AI-written summary · about

" chapters (11)

1. 0:00Decalf framework intro
2. 1:03Core language components
3. 2:47Program inequality for cost
4. 4:12Agda embedding proof
5. 5:17Phase distinction theorem
6. 6:43Adding probabilistic effects
7. 8:08Binomial distribution costs
8. 9:34Higher-order functions like map
9. 10:58Topos-theoretic semantics
10. 13:06Future work and conclusion
11. 14:11Q&A