Sciweavers

Share
TLCA
2009
Springer

Syntax for Free: Representing Syntax with Binding Using Parametricity

10 years 4 months ago
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.
Robert Atkey
Added 27 May 2010
Updated 27 May 2010
Type Conference
Year 2009
Where TLCA
Authors Robert Atkey
Comments (0)
books