Univalent Parametricity for Programming Modulo Equivalences
Date: Wed, February 26, 2020
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).
Jesper Cockx | Checking confluence of rewrite rules in Agda
Next: Arjan Mooij | Reducing the Complexity of Industrial Legacy Software