Intriniscly-Typed Interpretation of Linear Languages
summary
Defines an intrinsically-typed definitional interpreter for session-typed languages with linear channels, implemented in Agda so semantics are executable and type-safe by construction. Replaces explicit separation proof terms with a proof-relevant separation logic and a separation algebra extended with supply/demand, plus a linear state monad (and a free monad for concurrency). The paper ships interpreters and case-study semantics that compile and run from the repo; termination uses sized types where possible and fuel for threaded schedulers.
AI-written summary · about
chapters (11)
- 0:00Intrinsically-typed interpreters
- 1:52Linearity in session types
- 4:02Linearity enforcement challenges
- 5:49Shallow embedding with separation logic
- 7:33Simplified evaluation signatures
- 8:15Separation algebras and modalities
- 9:21State monads for linearity
- 10:28Resulting interpreters benefits
- 12:19Proof-relevant separation algebras
- 13:22Case studies and artifact
- 13:44Q&A
related talks
33mIntrinsically-Typed Definitional Interpreters à la Carte
32mIntrinsically Typed Sessions with Callbacks
23mCo-Contextual Typing Inference for the Linear π-Calculus in Agda (Extended Abstract)
19mTowards Tagless Interpretation of Stratified System F (Extended Abstract)
04mSeparated and Shared Effects in Higher-Order Languages
22mA Calculus of Inductive Linear Constructions
19mIll-Typed Programs Don't Evaluate
19mMechanizing Session-Types using a Structural View: Enforcing Linearity without ...