This thesis explores relational parametricity using fibrations. We present a complementary view of Reynolds's relational parametricity using the relations fibration. This approach allows us to uncover some of the hidden categorical structure present in Reynolds's original definitions and results, leading to new insights in the study of parametricity. In a similar vain we provide an alternative parametric model of System F using group actions, which has some novel differences to the standard relational model. We then alter the type system leading to a general categorical framework for type systems with dimension types. We develop some informative models of this type theory, including a model based on group actions that captures invariance under scaling.
|Date of Award||1 Dec 2015|
- University Of Strathclyde
|Supervisor||Neil Ghani (Supervisor) & Patricia Johann (Supervisor)|