Abstracts.2018.ParametricityDTT

Parametricity for Dependent Types

by Andrea Vezzosi

Reynolds [1] originally formulated relational parametricity as a model for System F. It formalized the intuition that polymorphic programs behave the same no matter what specific type they are applied to. In this talk we will explore how this notion has been extended to dependent types, where the distinction between types and programs is much less clear.

We will discuss the lightweight free theorems library [2] and some applications, but also its limitations with regard to the identity extension lemma. We will conclude with an overview of ParamDTT [3] and its distinction between "Π" and "∀".

[1] Types, Abstraction and Parametric Polymorphism In IFIP Congress (1983), pp. 513-523 by John C. Reynolds

[2] Lightweight Free Theorems

[3] Parametric Quantifiers for Dependent Type Theory doi: 10.1145/3110276