On Friday October 17, this site was moved to a new server, https://mw.hh.se. The original address will continue to work. Whithin a week or two this site will return to the original address. /Peo HH IT-dep
WG211/M19Brady
From WG 2.11
Jump to navigationJump to search
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).
