Projects per year
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 language | English |
---|---|
Title of host publication | Typed Lambda Calculi and Applications |
Subtitle of host publication | 9th International Conference, TLCA 2009, Brasilia, Brazil, July 1-3, 2009. Proceedings |
Publisher | Springer |
Pages | 35-49 |
Number of pages | 15 |
ISBN (Electronic) | 978-3-642-02273-9 |
ISBN (Print) | 978-3-642-02272-2 |
DOIs | |
Publication status | Published - 2009 |
Externally published | Yes |
Publication series
Name | Lecture Notes in Computer Science |
---|---|
Publisher | Springer Berlin Heidelberg |
Volume | 5608 |
ISSN (Print) | 0302-9743 |
ISSN (Electronic) | 1611-3349 |
Fingerprint
Dive into the research topics of 'Syntax for Free: Representing Syntax with Binding Using Parametricity'. Together they form a unique fingerprint.Projects
- 2 Finished
-
-
ReQueST: ReQueST:Resource Quantification in e-science Technologies.
Sannella, D., Aspinall, D., Gilmore, S. & Stark, I.
1/05/05 → 31/01/09
Project: Research