Till innehåll på sidan

Peter LeFanu Lumsdaine: Parametricity for type theories

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

Plats: Kräftriket, house 5, room 16

Medverkande: Peter LeFanu Lumsdaine

Exportera till kalender

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.