Write a Blog >>
ICFP 2018
Sun 23 - Sat 29 September 2018 St. Louis, Missouri, United States
Tue 25 Sep 2018 14:07 - 14:30 at Stifel Theatre - Proof Techniques and Mechanization Chair(s): Niki Vazou

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 Sep
Times are displayed in time zone: Guadalajara, Mexico City, Monterrey change

13:00 - 14:30
Proof Techniques and MechanizationResearch Papers at Stifel Theatre
Chair(s): Niki VazouUniversity of Maryland, USA
13:00
22m
Talk
MoSeL: A General, Extensible Modal Framework for Interactive Proofs in Separation Logic
Research Papers
Robbert KrebbersDelft University of Technology, Jacques-Henri JourdanCNRS, LRI, Université Paris-Sud, Ralf JungMPI-SWS, Joseph TassarottiCarnegie Mellon University, Jan-Oliver KaiserMPI-SWS, Amin Timanyimec-Distrinet KU-Leuven, Arthur CharguéraudInria, Derek DreyerMPI-SWS
DOI
13:22
22m
Talk
Mtac2: Typed Tactics for Backward Reasoning in Coq
Research Papers
Jan-Oliver KaiserMPI-SWS, Beta ZilianiFAMAF, UNC and CONICET, Robbert KrebbersDelft University of Technology, Yann Régis-GianasIRIF, University Paris Diderot and CNRS, France / INRIA PI.R2, Derek DreyerMPI-SWS
DOI
13:45
22m
Talk
Compositional Soundness Proofs of Abstract Interpreters
Research Papers
Sven KeidelDelft University of Technology, Netherlands, Casper Bach PoulsenDelft University of Technology, Sebastian ErdwegDelft University of Technology, Netherlands
DOI
14:07
22m
Talk
Equivalences for Free: Univalent Parametricity for Effective TransportDistinguished Paper
Research Papers
Nicolas TabareauInria, Éric TanterUniversity of Chile & Inria Paris, Matthieu SozeauInria
DOI