A Bunch of Sessions: A Propositions-as-Sessions Interpretation of Bunched Implications in
summary
A session-typed π-calculus extracted from the Logic of Bunched Implications, called πBI, implements a new runtime spawn primitive that duplicates providers (and their dependencies) and a drop/kill action for weakening. The paper gives a Curry–Howard correspondence, proves type preservation, deadlock-freedom and weak normalization for well-typed processes, provides an operationally sound and complete encoding of an affine λ-calculus, develops denotational semantics, and demonstrates provenance tracking for separated memory-cell protocols.
AI-written summary · about
chapters (9)
- 0:00Start
- 3:02Curry-Howard correspondences
- 4:06A process calculus
- 5:24The Logic of Bunched Implications
- 7:08From logics to session types
- 9:14Typing Communication and Linearity
- 14:09The Challenge with Contraction
- 16:33The Challenge with Weakening
- 18:54The meaning of types in BI
related talks
32mIntrinsically Typed Sessions with Callbacks
35mEvent-Driven Multiparty Session Actors
23mA Synthetic Reconstruction of Multiparty Session Types
19mMechanizing Session-Types using a Structural View: Enforcing Linearity without ...
37mClassical Processes in modern dress
23mCo-Contextual Typing Inference for the Linear π-Calculus in Agda (Extended Abstract)
22mProbabilistic Refinement Session Types
16mIntriniscly-Typed Interpretation of Linear Languages