A Deep Embedding of Parametric Polymorphism in Coq
Robert Atkey. A Deep Embedding of Parametric Polymorphism in Coq. In Workshop on Mechanising Metatheory. 2009.
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.
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.