Generic Programming with Univalence

Abstract: This project explores the programming applications of Homotopy Type Theory
(HoTT). In particular, we are interested in eliminating boilerplate code in a
systematic way by exploiting the principle of "reasoning up to isomorphism",
made possible by the univalence axiom in HoTT. A program written against
a concrete interface should be reusable against any other interface that
is in some sense equivalent to the original, and this reuse should happen
automatically, without any additional effort from the programmer.
We further explore a generalisation of HoTT, Directed Type Theory (DTT), which
enables reasoning about directed transformations, in the style of
(higher-dimensional) category theory. We believe this direction will provide
a framework for generalising and unifying the existing program-reuse
techniques, such as subtyping.

Category: functional programming / programming languages