Ups: Created page with "''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..."

2019-04-28T11:54:42Z

Created page with "''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..."

New page

''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).

WG211/M19Brady - Revision history

Ups: Created page with "''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..."