Fibrations and Logical Relations

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

• Claudio Hermida
• Tuesday 21 August 2012, 15:00-16:00
• CS 245.

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.

This talk is included in these lists:

• CS 245
• Lab Lunch

Note that ex-directory lists are not shown.