Thesis
Bifibrational parametricity : from zero to two dimensions
- Creator
- Rights statement
- Awarding institution
- University of Strathclyde
- Date of award
- 2017
- Thesis identifier
- T14509
- Person Identifier (Local)
- 201257497
- Qualification Level
- Qualification Name
- Department, School or Faculty
- 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.
- Resource Type
- DOI
- EThOS ID
- uk.bl.ethos.703525
- Date Created
- 2017
- Former identifier
- 9912542890302996
Relations
Items
| Thumbnail | Title | Date Uploaded | Visibility | Actions |
|---|---|---|---|---|
|
|
PDF of thesis T14509 | 2021-07-02 | Public | Download |