Syntax for free: representing syntax with binding using parametricity

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

18 Citations (Scopus)

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.
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

Fingerprint

Polymorphism
Isomorphic
Closed
Term
Parametric Model
Higher Order
Theorem
Demonstrate
Syntax
Model

Keywords

  • parametricity
  • syntax
  • parametric model

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
Atkey, Robert. / Syntax for free: representing syntax with binding using parametricity. Typed Lambda Calculi and Applications, 9th International Conference, TLCA 2009. editor / Pierre-Louis Curien. Vol. 5608 Springer, 2009. pp. 35-49 (Lecture Notes in Computer Science).
@inproceedings{b1d259814a64458390aef3beb7b0e74b,
title = "Syntax for free: representing syntax with binding using parametricity",
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.",
keywords = "parametricity , syntax, parametric model",
author = "Robert Atkey",
year = "2009",
doi = "10.1007/978-3-642-02273-9_5",
language = "English",
isbn = "978-3-642-02272-2",
volume = "5608",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "35--49",
editor = "Pierre-Louis Curien",
booktitle = "Typed Lambda Calculi and Applications, 9th International Conference, TLCA 2009",

}

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, Lecture Notes in Computer Science, vol. 5608, Springer, pp. 35-49. https://doi.org/10.1007/978-3-642-02273-9_5

Syntax for free: representing syntax with binding using parametricity. / Atkey, Robert.

Typed Lambda Calculi and Applications, 9th International Conference, TLCA 2009. ed. / Pierre-Louis Curien. Vol. 5608 Springer, 2009. p. 35-49 (Lecture Notes in Computer Science; Vol. 5608).

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

TY - GEN

T1 - Syntax for free: representing syntax with binding using parametricity

AU - Atkey, Robert

PY - 2009

Y1 - 2009

N2 - 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.

AB - 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.

KW - parametricity

KW - syntax

KW - parametric model

UR - http://www.springerlink.com/content/5381kl310044w356/

UR - http://personal.cis.strath.ac.uk/~raa/syntaxforfree.html

U2 - 10.1007/978-3-642-02273-9_5

DO - 10.1007/978-3-642-02273-9_5

M3 - Conference contribution book

SN - 978-3-642-02272-2

VL - 5608

T3 - Lecture Notes in Computer Science

SP - 35

EP - 49

BT - Typed Lambda Calculi and Applications, 9th International Conference, TLCA 2009

A2 - Curien, Pierre-Louis

PB - Springer

ER -

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