Picture of automobile manufacturing plant

Driving innovations in manufacturing: Open Access research from DMEM

Strathprints makes available Open Access scholarly outputs by Strathclyde's Department of Design, Manufacture & Engineering Management (DMEM).

Centred on the vision of 'Delivering Total Engineering', DMEM is a centre for excellence in the processes, systems and technologies needed to support and enable engineering from concept to remanufacture. From user-centred design to sustainable design, from manufacturing operations to remanufacturing, from advanced materials research to systems engineering.

Explore Open Access research by DMEM...

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 - Accepted Author Manuscript

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.