Syntax for Free: Representing Syntax with Binding Using Parametricity

Robert Atkey

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


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
Subtitle of host publication9th International Conference, TLCA 2009, Brasilia, Brazil, July 1-3, 2009. Proceedings
PublisherSpringer Berlin Heidelberg
Number of pages15
ISBN (Electronic)978-3-642-02273-9
ISBN (Print)978-3-642-02272-2
Publication statusPublished - 2009
Externally publishedYes

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin Heidelberg
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Dive into the research topics of 'Syntax for Free: Representing Syntax with Binding Using Parametricity'. Together they form a unique fingerprint.

Cite this