Evan Cavallo: Internal parametricity (and cubical type theory)

Abstract

Parametricity is a property of typed programming languages that makes it possible to separate interface from implementation: for a given interface, it provides a notion of relatedness between implementations such that any code written in terms of the interface will produce identical results if instantiated with related implementations. One can thereby freely switch between implementations without worrying this will affect the program output, or verify properties of an optimized implementation by checking that they hold of some simpler implementation.

Dependently typed programming languages have type systems that can capture complex properties of programs; for example, a sorting algorithm could be given a type requiring that it really does output a sorted version of its input. Recently, Bernardy and Moulin developed an "internally parametric" extension of dependent type theory in which parametricity can be used in the proofs of such properties. In this talk I'll introduce parametricity and describe how it can be internalized. I'll also briefly discuss my own work with Robert Harper on integrating internal parametricity with cubical type theory, a new approach to equality reasoning with dependent types.