Picture of a sphere with binary code

Making Strathclyde research discoverable to the world...

The Strathprints institutional repository is a digital archive of University of Strathclyde research outputs. It exposes Strathclyde's world leading Open Access research to many of the world's leading resource discovery tools, and from there onto the screens of researchers around the world.

Explore Strathclyde Open Access research content

Syntax for free: representing syntax with binding using parametricity

Atkey, Robert (2009) Syntax for free: representing syntax with binding using parametricity. In: Typed Lambda Calculi and Applications, 9th International Conference, TLCA 2009. Lecture Notes in Computer Science, 5608 . Springer, pp. 35-49. ISBN 978-3-642-02272-2

syntaxforfree.pdf - Submitted Version

Download (198kB) | Preview


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.