Syntax for Free: Representing Syntax with Binding Using Parametricity

We show that, in a parametric model of polymorphism, the type ∀α.((α → α) → α) → (α → α → α) → α is isomorphic to closed n 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.

• Type: Conference
• Year: 2009
• Where: TLCA
• Authors: Robert Atkey
• Keywords: Coq Proof Assistant, Isomorphic, Parametric Model, Theoretical Computer Science, TLCA 2009