TY - GEN
T1 - Syntax for free: representing syntax with binding using parametricity
AU - Atkey, Robert
PY - 2009
Y1 - 2009
N2 - 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.
AB - 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.
KW - parametricity
KW - syntax
KW - parametric model
UR - http://www.springerlink.com/content/5381kl310044w356/
UR - http://personal.cis.strath.ac.uk/~raa/syntaxforfree.html
U2 - 10.1007/978-3-642-02273-9_5
DO - 10.1007/978-3-642-02273-9_5
M3 - Conference contribution book
SN - 978-3-642-02272-2
VL - 5608
T3 - Lecture Notes in Computer Science
SP - 35
EP - 49
BT - Typed Lambda Calculi and Applications, 9th International Conference, TLCA 2009
A2 - Curien, Pierre-Louis
PB - Springer
ER -