WG211/M19Brady

Resource Safety with Linear Dependent Types by Edwin Brady

I will show progress on a new version of Idris, based on Quantitative Type Theory (QTT). QTT, developed by Bob Atkey and Conor McBride, is a type theory with dependent types and 'multiplicity' annotations which allow us to express how often a variable will be used as part of its type.

In this talk, I'll demonstrate interactive type-driven editing of resource aware programs in Idris, including the current state of type-directed progam synthesis, and show examples of how QTT can be used to represent state machines and resource usage protocols (e.g. session types).