Fibrational parametricity

Add to your list(s) Download to your calendar using vCal

• Neil Ghani, University of Strathclyde
• Thursday 18 April 2013, 10:00-11:00
• CS 245.

If you have a question about this talk, please contact Paul Levy.

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, parametrictiy 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 (operations, 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 is heavily related to, and influenced by, work of Reddy and Dunphy on reflexive graph parametricity.

This talk is part of the Theoretical computer science seminar series.

This talk is included in these lists:

• CS 245
• Computer Science Departmental Series
• Computer Science Distinguished Seminars
• Theoretical computer science seminar
• computer sience

Note that ex-directory lists are not shown.