Peter LeFanu Lumsdaine: Parametricity for type theories

Tid: On 2020-03-04 kl 10.00 - 11.45

Föreläsare: Peter LeFanu Lumsdaine

Plats: 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.

Innehållsansvarig:webmaster@math.kth.se
Tillhör: Institutionen för matematik
Senast ändrad: 2020-03-02