A Calculus of Inductive Linear Constructions

Explore a groundbreaking video presentation from TyDe 2023 introducing a Calculus of Inductive Linear Constructions (CILC). Delve into the innovative combination of linear types and dependent types, addressing a critical gap in linear dependent types research. Discover how CILC provides a general mechanism for defining sound linear inductive types, simplifying the encoding of various data structures and facilitating non-trivial program writing. Examine the standard meta theory of the calculus, its soundness, and its heap-based operational semantics demonstrating safe resource manipulation and memory cleanliness. Learn about the formalization and proof of correctness using the Coq Proof Assistant. Gain insights into dependent types, linear types, inductive types, and heap semantics through this 22-minute talk by Qiancheng Fu and Hongwei Xi from Boston University, presented at the ACM SIGPLAN-sponsored TyDe 2023 conference.

[TyDe'23] A Calculus of Inductive Linear Constructions