Equivalences for Free: Univalent Parametricity for Effective TransportDistinguished Paper
Homotopy Type Theory promises a unification of the concepts of equality and equivalence in Type Theory, through the introduction of the univalence principle. However, existing proof assistants based on type theory treat this principle as an axiom, and it is not yet clear how to extend them to handle univalence internally. In this paper, we propose a construction grounded on a univalent version of parametricity to bring the benefits of univalence to the programmer and prover, that can be used on top of existing type theories. In particular, univalent parametricity strengthens parametricity to ensure preservation of type equivalences. We present a lightweight framework implemented in the Coq proof assistant that allows the user to transparently transfer definitions and theorems for a type to an equivalent one, as if they were equal. Our approach handles both type and term dependency. We study how to maximize the effectiveness of these transports in terms of computational behavior, and identify a fragment useful for certified programming on which univalent transport is guaranteed to be effective.
Tue 25 SepDisplayed time zone: Guadalajara, Mexico City, Monterrey change
13:00 - 14:30 | Proof Techniques and MechanizationResearch Papers at Stifel Theatre Chair(s): Niki Vazou University of Maryland, USA | ||
13:00 22mTalk | MoSeL: A General, Extensible Modal Framework for Interactive Proofs in Separation Logic Research Papers Robbert Krebbers Delft University of Technology, Jacques-Henri Jourdan CNRS, LRI, Université Paris-Sud, Ralf Jung MPI-SWS, Joseph Tassarotti Carnegie Mellon University, Jan-Oliver Kaiser MPI-SWS, Amin Timany imec-Distrinet KU-Leuven, Arthur Charguéraud Inria, Derek Dreyer MPI-SWS DOI | ||
13:22 22mTalk | Mtac2: Typed Tactics for Backward Reasoning in Coq Research Papers Jan-Oliver Kaiser MPI-SWS, Beta Ziliani FAMAF, UNC and CONICET, Robbert Krebbers Delft University of Technology, Yann Régis-Gianas IRIF, University Paris Diderot and CNRS, France / INRIA PI.R2, Derek Dreyer MPI-SWS DOI | ||
13:45 22mTalk | Compositional Soundness Proofs of Abstract Interpreters Research Papers Sven Keidel Delft University of Technology, Netherlands, Casper Bach Poulsen Delft University of Technology, Sebastian Erdweg Delft University of Technology, Netherlands DOI | ||
14:07 22mTalk | Equivalences for Free: Univalent Parametricity for Effective TransportDistinguished Paper Research Papers DOI |