Dependent type systems offer a remarkable opportunity for programmers. Astonishingly, they can reflect the fact that validity of data often has something to do with other data. Shockingly, they can recognize that the tests which a program performs on data often have something to do with choosing the correct subsequent computation. Disturbingly, they can explain why a program's output often has something to do with its input.
This course will often give interested programmers something to do with dependent type systems. Based on the Epigram language, it will introduce new approaches to old problems, with accessible examples. Whilst we can use Epigram's type system as a kind of `logical scaffolding' for more traditional programs, this course will emphasize the design of data structures which naturally support correct programming `from the inside'. Working this way is fun, especially when your editing system exploits the fact that, uncannily, a program's structure often has something to do with its type.