A Deep Embedding of Parametric Polymorphism in Coq
Publication Information
Robert Atkey. A Deep Embedding of Parametric Polymorphism in Coq. In Workshop on Mechanising Metatheory. 2009.Abstract
We describe a deep embedding of System F inside Coq, along with a
denotational semantics that supports reasoning using Reynolds
parametricity. The denotations of
System F types are given exactly by objects of sort Set in Coq,
and the relations used to formalise Reynolds parametricity are Coq
predicates with values in Prop. A key feature of the model is
the extensive use of dependent types to maintain agreement between the
parts of the model. We use type dependency to represent
well-formedness of types and terms, and to keep track of the relation
between the denotations of types and the parametricity relations
between them.
We have used an extension of this formalisation in other research, where we proved that the parametric polymorphic representation of Higher-Order Abstract Syntax is adequate.
Additional Information
The model described in this paper was used to prove the adequacy of the polymorphic higher-order abstract syntax encoding of syntax with binding in a paper presented at TLCA in 2009.
The Coq development (tested with Coq8.4pl6) can be downloaded from the GitHub repository.