Alex Simpson: Fibrational Models for Relational Parametricity

Following on from my seminars in October and November, I shall present axiomatic structure for category-theoretic models of relational parametricity for polymorphic lambda-calculus, based on the notion of fibration. The structure is modular, and looks promising as a basis for generalisations to richer type theories, such as dependent type theories.

This is joint work with Neil Ghani and Fredrik Nordvall Forsberg of Strathclyde Univrsity, based on our paper "Comprehensive Relational Parametricity: Categorical Models and Type Theory", which is being presented at FoSSaCS 2016 this week