Mechanizing Session-Types using a Structural View: Enforcing Linearity without ...
summary
Claims a method that removes linear contexts by embedding linearity as local predicates, mechanizes a session-typed CP variant called structural classical processes (SCP), and proves adequacy between SCP and CP. Encoding uses LF with higher-order abstract syntax and the Beluga proof assistant, implements a Lin X P predicate to enforce channel linearity, and completes a type-preservation proof after three retries of encodings. Mechanization artifacts are available and evaluated (Zenodo / OOPSLA paper).
AI-written summary · about
chapters (7)
- 0:00Mechanizing session types
- 1:04Session type challenges
- 3:10Structural classical processes
- 6:01Enforcing linearity
- 9:12Beluga mechanization
- 13:06Structural vs linear contexts
- 15:35Q&A
related talks
16mSoundly Handling Linearity
32mIntrinsically Typed Sessions with Callbacks
37mClassical Processes in modern dress
45mLogic Meta Programming for Functional Languages
23mCo-Contextual Typing Inference for the Linear π-Calculus in Agda (Extended Abstract)
31mIs there a use for linear types?
50mA Type-Theoretic Framework for Certified Meta-programming
53mSemantics-based program manipulation in the age of LLMs