Co-Contextual Typing Inference for the Linear π-Calculus in Agda (Extended Abstract)
summary
Bottom-up inference traverses processes and expressions, returning contexts with metavariables and a constraint set rather than a single solution, implemented as an Agda prototype that generates deferred splitting constraints for linear usage annotations 0/1/ω. The work proves soundness and completeness relative to any substitution satisfying those constraints, identifies usage polymorphism as the reason eager solving fails, and sketches two fixes: a syntax-shaped constraint tree or an Agda encoding that eagerly emits one-sided splits.
AI-written summary · about
chapters (13)
- 0:00Introduction
- 0:13Recap
- 3:03Processes
- 4:53Types
- 7:02Inference Types
- 8:12Equality Constraints
- 9:10Usage Annotations
- 11:21Typing Rules
- 13:02Context Splits
- 16:38Inference
- 18:30Soundness
- 19:20completeness
- 19:58summary
related talks
22mA Calculus of Inductive Linear Constructions
19mType Inference Logics
25mFormalizing pi-Calculus in Guarded Cubical Agda
24mLocal Contextual Type Inference
16mIntriniscly-Typed Interpretation of Linear Languages
14mType-Sensitive Algebraic Macros
21mSeamless Scope-Safe Metaprogramming Through Polymorphic Subtype Inference (Short Paper)
13mOne-Pass CPS Translation of Dependent Types (Talk Proposal)