Parametricity in an Impredicative Sort

Abstract : Reynold's abstraction theorem is now a well-established result for a large class of type systems. We propose here a definition of relational parametricity and a proof of the abstraction theorem in the Calculus of Inductive Constructions (CIC), the underlying formal language of Coq, in which parametricity relations' codomain is the impredicative sort of propositions. To proceed, we need to refine this calculus by splitting the sort hierarchy to separate informative terms from non-informative terms. This refinement is very close to CIC, but with the property that typing judgments can distinguish informative terms. Among many applications, this natural encoding of parametricity inside CIC serves both theoretical purposes (proving the independence of propositions with respect to the logical system) as well as practical aspirations (proving properties of finite algebraic structures). We finally discuss how we can simply build, on top of our calculus, a new reflexive Coq tactic that constructs proof terms by parametricity.
Type de document :
Communication dans un congrès
Patrick Cégielski and Arnaud Durand. CSL - 26th International Workshop/21st Annual Conference of the EACSL - 2012, Sep 2012, Fontainebleau, France. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 16, pp.381-395, 2012, CSL. 〈10.4230/LIPIcs.CSL.2012.399〉
Liste complète des métadonnées

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

https://hal.inria.fr/hal-00730913
Contributeur : Chantal Keller <>
Soumis le : jeudi 27 septembre 2012 - 12:20:20
Dernière modification le : mercredi 14 novembre 2018 - 15:30:04
Document(s) archivé(s) le : vendredi 28 décembre 2012 - 02:45:10

Fichiers

paramath.pdf
Fichiers éditeurs autorisés sur une archive ouverte

Identifiants

Citation

Chantal Keller, Marc Lasson. Parametricity in an Impredicative Sort. Patrick Cégielski and Arnaud Durand. CSL - 26th International Workshop/21st Annual Conference of the EACSL - 2012, Sep 2012, Fontainebleau, France. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 16, pp.381-395, 2012, CSL. 〈10.4230/LIPIcs.CSL.2012.399〉. 〈hal-00730913〉

Partager

Métriques

Consultations de la notice

468

Téléchargements de fichiers

331