Split Decisions: Explicit Contexts for Substructural Languages

on YouTube ↗28m

" summary

Contexts as Resource Vectors frames contexts as lists whose entries carry tags from a resource algebra so consumption means changing tags rather than removing entries. The infrastructure CARVe is implemented in Beluga, proves cut elimination for the linear sequent calculus, shows equivalence between sequent and bidirectional linear λ‑calculi, mechanizes CP with subject reduction and an adequacy proof to SCP, reuses about 40–80% of mechanization via the shared primitives, and ships artifacts (DOI available).

AI-written summary · about

" chapters (16)

1. 0:00Introduction
2. 0:22Substructural systems
3. 1:47Substructural logics applications
4. 3:14Mechanizing challenges
5. 3:59Carve infrastructure
6. 5:24Context modeling approaches
7. 8:17Carve's resource annotations
8. 10:04Resource algebras
9. 12:33Cut rule reformulation
10. 13:16Implicit exchange handling
11. 15:04Lolly left rule reformulation
12. 15:46Context leaves management
13. 17:31Beluga case studies
14. 19:17Carve's contributions summary
15. 20:20Future directions
16. 21:05Question and answer session