Types, categories, actions

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.

Name dc:type.qualificationname

phd

Level dc:type.qualificationlevel

doctoral-pg

Grantor dc:publisher.institution

University of Strathclyde

Year dc:date.issued

2016

Author dc:creator

• Revell, Timothy

DOI

10.48730/407e-nn33

Identifier

T14245

Author Identifier

201266665

OAI identifier oai:identifier

oai:strathclyde:d791sg22v