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 - Submitted Version
Download (193Kb) | 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
    Related URLs:
    Depositing user: Pure Administrator
    Date Deposited: 12 Nov 2011 11:05
    Last modified: 06 Sep 2014 13:40
    URI: http://strathprints.strath.ac.uk/id/eprint/34483

    Actions (login required)

    View Item

    Fulltext Downloads: