Parametricity in an Impredicative SortReport as inadecuate

Parametricity in an Impredicative Sort - Download this document for free, or read online. Document in PDF available to download.

1 TYPICAL - Types, Logic and computing LIX - Laboratoire d-informatique de l-École polytechnique Palaiseau, Inria Saclay - Ile de France, Polytechnique - X, CNRS - Centre National de la Recherche Scientifique : UMR 2 LIX - Laboratoire d-informatique de l-École polytechnique Palaiseau 3 LIP - Laboratoire de l-Informatique du Parallélisme

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.

Keywords : Calculus of Inductive Constructions parametricity impredicativity Coq universes

Author: Chantal Keller - Marc Lasson -



Related documents