Syntax for free: representing syntax with binding using parametricity
Atkey, Robert; Curien, Pierre-Louis, ed. (2009) Syntax for free: representing syntax with binding using parametricity. In: Typed Lambda Calculi and Applications, 9th International Conference, TLCA 2009. Lecture Notes in Computer Science, 5608 . Springer, pp. 35-49. ISBN 978-3-642-02272-2 (https://doi.org/10.1007/978-3-642-02273-9_5)
Preview |
PDF.
Filename: syntaxforfree.pdf
Accepted Author Manuscript Download (198kB)| 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: Book Section ID code: 34483 Dates: DateEvent2009PublishedSubjects: Science > Mathematics > Electronic computers. Computer science Department: Faculty of Science > Computer and Information Sciences Depositing user: Pure Administrator Date deposited: 12 Nov 2011 11:05 Last modified: 24 Mar 2024 01:20 Related URLs: URI: https://strathprints.strath.ac.uk/id/eprint/34483