Really Natural Linear Indexed Type Checking
Arthur Azevedo de Amorim, Marco Gaboardi, Emilio Jesús Gallego Arias, Justin Hsu · 2014
Recent works have shown the power of linear indexed type systems for enforcing complex program properties. These systems combine linear types with a language of type-level indices, allowing more fine-grained analyses. Such systems have been fruitfully applied in diverse domains, including implicit complexity and differential privacy.