Skip to main content

Peter LeFanu Lumsdaine: Parametricity for type theories

Time: Wed 2020-03-04 10.00 - 11.45

Lecturer: Peter LeFanu Lumsdaine

Location: Kräftriket, house 5, room 16

Abstract

“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.

Page responsible:webmaster@math.kth.se
Belongs to: Department of Mathematics
Last changed: Mar 02, 2020