Strathprints logo
Strathprints Home | Open Access | Browse | Search | User area | Copyright | Help | Library Home | SUPrimo

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

[img]
Preview
PDF
syntaxforfree.pdf - Submitted Version

Download (198kB) | Preview

Abstract

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.

Item type: Book Section
ID code: 34483
Keywords: parametricity , syntax, parametric model, Electronic computers. Computer science
Subjects: Science > Mathematics > Electronic computers. Computer science
Department: Faculty of Science > Computer and Information Sciences
Depositing user: Pure Administrator
Date Deposited: 12 Nov 2011 11:05
Last modified: 18 Jun 2015 06:06
Related URLs:
URI: http://strathprints.strath.ac.uk/id/eprint/34483

Actions (login required)

View Item View Item