Separated and Shared Effects in Higher-Order Languages
summary
Proposes two higher-order languages, λ^1_{INI} with a linear type system that distinguishes independent and possibly-dependent pairs, and λ^2_{INI}, a two-level stratified LNL-style language with a functorial layer between a copy-delete category and a symmetric monoidal closed linear category. Gives a categorical semantics where an applicative functor models taking two independent distributions to their joint, lists concrete models (vector-space/coherence style models and algebras for commutative monads), and proves that closed terms of type M τ1 × M τ2 factor into marginals so the semantics is the product distribution.
AI-written summary · about
chapters (6)
- 0:00Research Context
- 0:52Bunched Typing
- 1:40A Two-Level Language
- 2:28Categorical Semantics
- 3:08Concrete Models
- 3:42Soundness Theorem
related talks
15mStable Relations and Abstract Interpretation of Higher-Order Programs
16mIntriniscly-Typed Interpretation of Linear Languages
30mContinuations and Coexponentials
27mThe Relative Monadic Metalanguage
19mCombining Dependency, Grades, and Adjoint Logic
26m2-Functoriality of Initial Semantics, and Applications
24mClassical Notions of Computation and the Hasegawa-Thielecke Theorem
20mA Dependent Type Theory for Meta-programming with Intensional Analysis