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
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Aydemir, B.E., Charguéraud, A., Pierce, B.C., Pollack, R., Weirich, S.: Engineering formal metatheory. In: Necula, G.C., Wadler, P. (eds.) POPL, pp. 3–15. ACM Press, New York (2008)
Carette, J., Kiselyov, O., Shan, C.-c.: Finally tagless, partially evaluated. In: Shao, Z. (ed.) APLAS 2007. LNCS, vol. 4807, pp. 222–238. Springer, Heidelberg (2007)
Chlipala, A.J.: Parametric higher-order abstract syntax for mechanized semantics. In: ICFP, pp. 143–156 (2008)
Coquand, T., Huet, G.: Constructions: A higher order proof system for mechanizing mathematics. In: Buchberger, B. (ed.) EUROCAL 1985. LNCS, vol. 203, pp. 151–184. Springer, Heidelberg (1985)
de Bruijn, N.G.: Lambda-calculus notation with nameless dummies: a tool for automatic formula manipulation with application to the Church-Rosser theorem. Indag. Math. 34, 381–392 (1972)
Despeyroux, J., Felty, A.P., Hirschowitz, A.: Higher-Order Abstract Syntax in Coq. In: Dezani-Ciancaglini, M., Plotkin, G. (eds.) TLCA 1995. LNCS, vol. 902, pp. 124–138. Springer, Heidelberg (1995)
Gabbay, M., Pitts, A.M.: A New Approach to Abstract Syntax Involving Binders. In: LICS, pp. 214–224 (1999)
Harper, R., Licata, D.R.: Mechanizing metatheory in a logical framework. J. Funct. Program. 17(4-5), 613–673 (2007)
Hofmann, M.: Semantical Analysis of Higher-Order Abstract Syntax. In: LICS, pp. 204–213 (1999)
Izumi, T.: The Theory of Parametricity in Lambda Cube. Technical Report 1217, RIMS Kokyuroku (2001)
Licata, D.R., Zeilberger, N., Harper, R.: Focusing on Binding and Computation. In: LICS, pp. 241–252. IEEE Computer Society, Los Alamitos (2008)
Moggi, E., Sabry, A.: Monadic encapsulation of effects: a revised approach (extended version). J. Funct. Program. 11(6), 591–627 (2001)
Pfenning, F., Elliott, C.: Higher-Order Abstract Syntax. In: PLDI, pp. 199–208 (1988)
Pfenning, F., Lee, P.: Metacircularity in the polymorphic λ-calculus. Theoretical Computer Science 89, 137–159 (1991)
Plotkin, G.D.: Lambda-Definability in the Full Type Hierarchy. In: Seldin, J.P., Hindley, J.R. (eds.) To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pp. 363–373. Academic Press, London (1980)
Reynolds, J.C.: Types, Abstraction and Parametric Polymorphism. In: IFIP Congress, pp. 513–523 (1983)
Rhiger, M.: A foundation for embedded languages. ACM Trans. Program. Lang. Syst. 25(3), 291–315 (2003)
Washburn, G., Weirich, S.: Boxes go bananas: Encoding higher-order abstract syntax with parametric polymorphism. J. Funct. Program. 18(1), 87–140 (2008)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Atkey, R. (2009). Syntax for Free: Representing Syntax with Binding Using Parametricity. In: Curien, PL. (eds) Typed Lambda Calculi and Applications. TLCA 2009. Lecture Notes in Computer Science, vol 5608. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-02273-9_5
Download citation
DOI: https://doi.org/10.1007/978-3-642-02273-9_5
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-02272-2
Online ISBN: 978-3-642-02273-9
eBook Packages: Computer ScienceComputer Science (R0)