Univalent Parametricity for Programming Modulo Equivalences

Lucas Escot


Date: Wed, February 26, 2020
Time: 12:00
Room: COLLOQUIUMZAAL 0.E420


Univalent Parametricity is a new heterogenous extension of parametricity strengthened with univalence. It makes it possible to prove & program modulo equivalences, and transfer definitions and theorems between equivalent types as if they were equal. This allows one to easily switch between representations that are easy to reason about and computationally-efficient representations, seamlessly. We will see how univalence & parametricity alone cannot transfer proofs as one would hope, and how it is made possible with univalent parametricity. Then I will talk about the current implementation of Univalent Parametricity in Coq, and the WIP re-implementation I’ve been doing using MetaCoq, a framework which allows metaprogramming in Coq (among other things).

Previous: Jesper Cockx |
Next: Arjan Mooij |