Bifibrational parametricity : from zero to two dimensions

  • Federico Orsanigo

Student thesis: Doctoral Thesis

Abstract

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 Award1 Oct 2016
LanguageEnglish
Awarding Institution
  • University Of Strathclyde
SupervisorNeil Ghani (Supervisor) & Clemens Kupke (Supervisor)

Cite this