Modal Logics and Types: Looking Back and Looking Forward

on YouTube ↗01h 03m

" summary

Shows that modal types make runtime code generation, staging and partial evaluation precise by decomposing S4 into up/down shifts (quotation = box as up then down), using types to guarantee staging and compile-time source extraction, and modeling temporal staging (Rowan Davies) as modes. Introduces adjoint logic and substructural adjoint logic with modes and shifts, proves cut elimination and standard type-safety results, reports concrete encodings for monads, lax/ghost code and session-style concurrency, and notes remaining puzzles (diamond, polarization, polymorphism).

AI-written summary · about

" chapters (19)

1. 0:00Start
2. 1:44Compiling the Polymorphic Lambda Calculus
3. 2:39Lightweight Runtime Cogeneration
4. 3:20Deferred Compilation
5. 4:04The Power Function
6. 5:51Power Function
7. 12:29Elimination Rule
8. 13:21Stepping Rules
9. 18:58Stratify the Syntax
10. 26:51Natural Deduction
11. 31:23Origin of Adjoint Logic
12. 33:41Rules for the Connectors
13. 35:21The Rules of Adjoint Logic
14. 41:54The Canonical Forms Theorem
15. 47:01The Adjoint Approach and the Linear Logic Approach
16. 47:48Substructural Android Logic
17. 49:09Substructural Adjoint Logic
18. 58:03Can the Substrate Logic Restrict Ordered Premises in Addition to Raping and Contraction
19. 1:01:44Is There a Way of Mixing Intuitionistic and the Classical Logic in this Framework