Skip to main content
To KTH's start page To KTH's start page

Peter LeFanu Lumsdaine: Parametricity for type theories

Time: Wed 2020-03-04 10.00 - 11.45

Location: Kräftriket, house 5, room 16

Participating: Peter LeFanu Lumsdaine

Export to calendar


“Parametricity” refers to an important class of results and properties of type theories, especially as used in programming languages, where the consequences of parametricity are known as “free theorems”.

The classic example says that in a polymorphic type theory (e.g. System F) with list types, any polymorphic function [ f : forall A, list A —> list A ] must be *natural* in its type argument, in that for any function [ g : A —> B ], it will satisfy [ (f B) . (listmap g) = (listmap g) . (f A) ].

Technically, parametricity results are often proved using *relational* and similar models of type theories, and variants. In this expository seminar, I will survey parametricity results and their proofs for several type theories.