A Calculus of Inductive Linear Constructions
summary
A new calculus combines linear and dependent types with inductive typing schemes and a guarded fixpoint plus case instead of ordinary induction for linear data to preserve no-contraction guarantees. The paper proves confluence, subject reduction and normalization and gives a heap-based operational semantics that shows linear values are memory safe and memory clean. Most meta-theory is formalized in Coq, and a prototype compiler (artifacts available) runs and exercises the design.
AI-written summary · about
chapters (14)
- 0:00Type driven development intro
- 0:42Calculus overview
- 2:07Background on Calculus of Inductive Constructions
- 3:12Stateful programming in dependent types
- 4:17Linear logic intro
- 6:06Limitations of linear Lambda
- 6:48Intrinsic modality in CILC
- 7:31Universe hierarchy
- 9:22Function types with modality
- 10:27Encoding data types
- 11:52Induction principles challenges
- 13:17Guarded fix points
- 14:45Conclusion
- 15:49Q&A
related talks
23mCo-Contextual Typing Inference for the Linear π-Calculus in Agda (Extended Abstract)
13mInductive Synthesis of Inductive Heap Predicates
19mType Inference Logics
19mIll-Typed Programs Don't Evaluate
20mCoq a la Carte: A Practical Approach to Modular Syntax With Binders
14mA Limited Case for Reification by Type Inference
27mCanonicity for Indexed Inductive-Recursive Types
11mLocal algebraic effect theories