We show that, in a parametric model of polymorphism, the type ∀ α. ((α → α) → α) → (α → α → α) → α is isomorphic to closed de Bruijn terms. That is, the type of closed higher-order abstract syntax terms is isomorphic to a concrete representation. To demonstrate the proof we have constructed a model of parametric polymorphism inside the Coq proof assistant. The proof of the theorem requires parametricity over Kripke relations. We also investigate some variants of this representation.
|Title of host publication||Typed Lambda Calculi and Applications, 9th International Conference, TLCA 2009|
|Number of pages||15|
|Publication status||Published - 2009|
|Name||Lecture Notes in Computer Science|
- parametric model