Syntax for free: representing syntax with binding using parametricity

Research output: Chapter in Book/Report/Conference proceedingConference contribution book

19 Citations (Scopus)
34 Downloads (Pure)

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.
Original languageEnglish
Title of host publicationTyped Lambda Calculi and Applications, 9th International Conference, TLCA 2009
EditorsPierre-Louis Curien
PublisherSpringer
Pages35-49
Number of pages15
Volume5608
ISBN (Print)978-3-642-02272-2
DOIs
Publication statusPublished - 2009

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume5608

Keywords

  • parametricity
  • syntax
  • parametric model

Fingerprint Dive into the research topics of 'Syntax for free: representing syntax with binding using parametricity'. Together they form a unique fingerprint.

  • Cite this

    Atkey, R. (2009). Syntax for free: representing syntax with binding using parametricity. In P-L. Curien (Ed.), Typed Lambda Calculi and Applications, 9th International Conference, TLCA 2009 (Vol. 5608, pp. 35-49). (Lecture Notes in Computer Science; Vol. 5608). Springer. https://doi.org/10.1007/978-3-642-02273-9_5