In this thesis we use bifibrations in order to study relational parametricity. There are three main contributions in this thesis. First, through the lenses of bifibrations, we give a new framework for models of parametricity. This allows us to make some of the underlying categorical structure in Reynolds' original work clearer. Using the same approach we then give a universal property for the interpretation of forall types: they are characterized as terminal objects in a certain category. The universal property permits us to prove both Reynolds' Identity Extension Lemma and Abstraction Theorem. The third contribution consists in defining two-dimensional parametricity. The insight derived from the bifibrational approach leads to a generalization of parametricity to proof relevant relations, incorporating higher-dimensional relations between relations. We call the resulting theory two-dimensional parametricity.
| Date of Award | 27 Jan 2017 |
|---|
| Original language | English |
|---|
| Awarding Institution | - University Of Strathclyde
|
|---|