Monadic and Comonadic Aspects of Dependency Analysis
summary
Presents GMCC, an alternative dependency calculus that is both monadic and comonadic, built from graded monads/comonads over a bicartesian closed category and shown sound and complete against a class of categorical models. Shows a translation proving GMCC under 13 restrictions is equivalent to a terminating fragment of DCC, explains DCC’s nonstandard bind and protection judgment as instances of monad algebras, and gives novel soundness proofs using monoidal functors; GMCCE then subsumes DCC and λ◦.
AI-written summary · about
chapters (5)
- 0:00Start
- 0:50Dependency Analysis: Basics
- 4:21Dependency Analysis: Calculus-II
- 10:39DCC: Limitations and Our Contributions
- 12:12Our Key Insights
related talks
19mCombining Dependency, Grades, and Adjoint Logic
34mGraded Monads and Type-Level Programming for Dependence Analysis
34mAdditive Cellular Automata Graded-Monadically
15mMonadification of Attribute Grammars
27mThe Relative Monadic Metalanguage
27mPractical Extensions for Graded Monads
14mRecovering Purity with Comonads and Capabilities
24mClassical Notions of Computation and the Hasegawa-Thielecke Theorem