Equivalences for Free: Univalent Parametricity for Effective Transport

Nicolas Tabareau 1, 2 Éric Tanter 3, 4 Matthieu Sozeau 5, 6
1 GALLINETTE - Gallinette : vers une nouvelle génération d'assistant à la preuve
Inria Rennes – Bretagne Atlantique , LS2N - Laboratoire des Sciences du Numérique de Nantes
5 PI.R2 - Design, study and implementation of languages for proofs and programs
Inria de Paris, CNRS - Centre National de la Recherche Scientifique, UPD7 - Université Paris Diderot - Paris 7, PPS - Preuves, Programmes et Systèmes
Abstract : 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. This work paves the way to easier-to-use environments for certified programming by supporting seamless programming and proving modulo equivalences.
Type de document :
Article dans une revue
Proceedings of the ACM on Programming Languages, ACM, 2018, ICFP'18, pp.1-29. 〈10.1145/3234615〉
Liste complète des métadonnées

Littérature citée [12 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01559073
Contributeur : Nicolas Tabareau <>
Soumis le : mardi 17 juillet 2018 - 09:13:29
Dernière modification le : jeudi 13 décembre 2018 - 22:05:41
Document(s) archivé(s) le : jeudi 18 octobre 2018 - 12:38:43

Fichier

main_icfp.pdf
Publication financée par une institution

Identifiants

Citation

Nicolas Tabareau, Éric Tanter, Matthieu Sozeau. Equivalences for Free: Univalent Parametricity for Effective Transport. Proceedings of the ACM on Programming Languages, ACM, 2018, ICFP'18, pp.1-29. 〈10.1145/3234615〉. 〈hal-01559073v5〉

Partager

Métriques

Consultations de la notice

626

Téléchargements de fichiers

252