University of Birmingham > Talks@bham > Lab Lunch > Fibrations and Logical Relations

Fibrations and Logical Relations

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

If you have a question about this talk, please contact Dan Ghica.

Unusual time and place!

Logical relations are a widely used concept in type theory as an orgnizational technique to prove various properties. Most prominenty, Reynolds used them in the context of polymorphic lambda calculus to formulate the pricniple of ‘relational parametricity’, which has many valuable consequences (validity of various impredicative encodings and associated (co)induction principles among others).,

In this survey talk, we analyse all this categorically, exploiting the technology of fibred category theory to provide a uniform basis on which to analyse the relevant structures underpinning the above calculi and their associated logics. We show also how the theory extends to other settings of interest like multicategories, bicategories of relations (and modal logic), etc.

This talk is part of the Lab Lunch series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


Talks@bham, University of Birmingham. Contact Us | Help and Documentation | Privacy and Publicity.
talks@bham is based on from the University of Cambridge.