Generic Programming with Univalence

Lead Research Organisation: Imperial College London
Department Name: Dept of Computing


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


10 25 50

Studentship Projects

Project Reference Relationship Related To Start End Student Name
EP/N509486/1 01/10/2016 31/03/2022
2347778 Studentship EP/N509486/1 01/10/2019 30/09/2021 Csongor Kiss