The Duality of λ-Abstraction

on YouTube ↗19m

" summary

Presents a concrete extension of call‑by‑value simply‑typed lambda calculus with covalues, coabstraction and coapplication, claiming that inserting double negations via the continuation monad yields nondegenerate coexponentials that dualize functions; gives an equational theory that axiomatizes control effects and proves completeness, provides a computational interpretation as speculative execution and backtracking, derives classical control operators and encodes common control patterns, and ships an interpreter and artifacted examples (SAT search, effect‑handler library) that demonstrate the ideas.

AI-written summary · about

" chapters (17)

1. 0:00Introduction
2. 0:26Motivation for dualizing lambda calculus
3. 1:09Dualizing currying puzzle
4. 3:39Solution via call-by-value
5. 5:04Programming with co-curry and co-anchor
6. 6:10Categorical foundations
7. 7:11Introducing λλ-calculus
8. 8:37Typing rules and logic
9. 9:21Algebra of co-functions
10. 10:26Deriving control operators
11. 11:11Intuitionistic versus classical sums
12. 12:56Short-circuiting multiplication example
13. 14:46Classical vs intuitionistic sums
14. 15:27Categorical and logical implications
15. 16:29Practical applications and interpreter
16. 16:51Conclusion and future work
17. 17:39Q&A