Classical Notions of Computation and the Hasegawa-Thielecke Theorem
summary
Defines a polarized effect calculus called linear classical L-calculus and shows composition can fail associativity when call-by-value and call-by-name coexist, so standard categorical models break. Builds a new notion of adjunction between graph morphisms and the dialogue duploid / non-associative symmetric monoidal closed structures, gives both syntactic and denotational models (including a finite distribution/probability example), constructs a syntactic dialogue duploid, and proves the Hasegawa-Thielecke theorem (central maps = thunkable maps) in that setting.
AI-written summary · about
chapters (12)
- 0:00Introduction
- 1:41Effects and evaluation order
- 3:34Duploid construction
- 6:05λ-calculus and polarized types
- 8:37Shifts in polarized categories
- 11:01Models of effects and adjunctions
- 13:44Probability and centrality example
- 16:28Contributions and future work
- 19:19Q&A: Hasegawa-Thielecke theorem
- 20:23Q&A: Adjunctions in non-associative categories
- 21:50Q&A: Non-associative structures
- 23:59Closing remarks
related talks
45mA categorical view of computational effects
14mAdequacy for Algebraic Effects Revisited
20mFully Abstract Models for Effectful λ-Calculi via Category-Theoretic Logica
37mClassical Processes in modern dress
22mAlgebraic Effects Meet Hoare Logic in Cubical Agda
30mContinuations and Coexponentials
11mLocal algebraic effect theories
29mLogical Relations for Effect Capabilities