Fibrational Parametricity

Neil Ghani

(University of Strathclyde)

Parametricity, also known as logical relations is a fundamental concept within programming languages designed to capture the idea that programs map related inputs to related outputs. Originally formulated by John Reynolds in the 1970s, parametricity has been a key tool in reasoning about programming languages ever since. However, as programming languages have advanced, parametricity has struggled to keep up. I think that part of the reason for this is that its not really clear what parametricity really is. We have lots of specific constructions of what a parametric model is but not overarching theory which can then be instantiated to a variety of different settings (operational, game-theoretic, constructive, domain theoretic etc).

In this talk I'll explain some work we have been doing in Strathclyde recently whose goal is to suggest that while the usual semantics of programming languages can be given abstractly in terms of a categorical universe using concepts such as categories, functors and natural transformations, parametricity amounts to working in a fibrational universe consisting of fibred categories, fibred functors and fibred natural transformations. This work forms the basis of a new EPSRC 4-year grant so anyone interested in applying for the associated RA position is particularly welcome to attend.
Monday 29th April 2013, 14:00
Far-134 (video conferencing room)
Department of Computer Science