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. [Proceedings Paper]

[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: Proceedings Paper
    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: 20 Jul 2013 21:36
    URI: http://strathprints.strath.ac.uk/id/eprint/34483

    Actions (login required)

    View Item

    Fulltext Downloads: