Robert Atkey, from TLCA 2009, available from Robert Atkey’s website.

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.

Slides from the TLCA presentation are available here.

### Like this:

Like Loading...

*Related*

As usual, here’s how to count variable occurrences with the technique introduced in this paper.