Abstract
This paper presents GMeta: a generic framework for first-order representations of variable binding that provides once and for all many of the so-called infrastructure lemmas and definitions required in mechanizations of formal metatheory. The key idea is to employ datatype-generic programming (DGP) and modular programming techniques to deal with the infrastructure overhead. Using a generic universe for representing a large family of object languages we define datatype-generic libraries of infrastructure for first-order representations such as locally nameless or de Bruijn indices. Modules are used to provide templates: a convenient interface between the datatype-generic libraries and the end-users of GMeta. We conducted case studies based on the POPLmark challenge, and showed that dealing with challenging binding constructs, like the ones found in System F < :, is possible with GMeta. All of GMeta’s generic infrastructure is implemented in the Coq theorem prover. Furthermore, due to GMeta’s modular design, the libraries can be easily used, extended, and customized by users.
This work was supported by the Engineering Research Center of Excellence Program of Korea Ministry of Education, Science and Technology(MEST)/National Research Foundation of Korea(NRF) (Grants R11-2008-007-01002-0 and 2010-0001717).
Chapter PDF
Similar content being viewed by others
Keywords
References
Altenkirch, T., McBride, C.: Generic programming within dependently typed programming. In: IFIP TC2/WG2.1 Working Conference on Generic Programming (2003)
Altenkirch, T., Reus, B.: Monadic Presentations of Lambda Terms Using Generalized Inductive Types. In: Flum, J., Rodríguez-Artalejo, M. (eds.) CSL 1999. LNCS, vol. 1683, pp. 453–468. Springer, Heidelberg (1999)
Aydemir, B., Weirich, S., Zdancewic, S.: Abstracting syntax. Technical Report MS-CIS-09-06, University of Pennsylvania (2009)
Aydemir, B.E., Weirich, S.: LNgen: Tool Support for Locally Nameless Representations (2009) (Unpublished manuscript)
Aydemir, B.E., Bohannon, A., Fairbairn, M., Foster, J.N., Pierce, B.C., Sewell, P., Vytiniotis, D., Washburn, G., Weirich, S., Zdancewic, S.: Mechanized Metatheory for the Masses: The PoplMark Challenge. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol. 3603, pp. 50–65. Springer, Heidelberg (2005)
Aydemir, B.E., Charguéraud, A., Pierce, B.C., Pollack, R., Weirich, S.: Engineering formal metatheory. In: POPL 2008 (2008)
Boutin, S.: Using Reflection to Build Efficient and Certified Decision Procedures. In: Ito, T., Abadi, M. (eds.) TACS 1997. LNCS, vol. 1281, pp. 515–529. Springer, Heidelberg (1997)
Cheney, J.: Scrap your nameplate (functional pearl). In: ICFP 2005 (2005)
Chlipala, A.: A certified type-preserving compiler from lambda calculus to assembly language. In: PLDI 2007 (2007)
Chlipala, A.: Parametric higher-order abstract syntax for mechanized semantics. In: ICFP 2008 (2008)
The Coq Development Team. The Coq Proof Assistant Reference Manual, Version 8.2 (2009), http://coq.inria.fr
de Bruijn, N.G.: Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the church-rosser theorem. Indagationes Mathematicae (Proceedings) 75(5), 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)
Dybjer, P.: Inductive families. Formal Aspects of Computing 6, 440–465 (1997)
Dybjer, P., Setzer, A.: A Finite Axiomatization of Inductive-Recursive Definitions. In: Girard, J.-Y. (ed.) TLCA 1999. LNCS, vol. 1581, pp. 129–146. Springer, Heidelberg (1999)
Dybjer, P., Setzer, A.: Indexed Induction-Recursion. In: Kahle, R., Schroeder-Heister, P., Stärk, R.F. (eds.) PTCS 2001. LNCS, vol. 2183, pp. 93–113. Springer, Heidelberg (2001)
Gacek, A.: The Abella Interactive Theorem Prover (System Description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 154–161. Springer, Heidelberg (2008)
Harper, R., Honsell, F., Plotkin, G.: A framework for defining logics. J. ACM 40(1), 143–184 (1993)
Hinze, R., Jeuring, J.: Generic Haskell: Practice and Theory. In: Backhouse, R., Gibbons, J. (eds.) Generic Programming SS 2002. LNCS, vol. 2793, pp. 1–56. Springer, Heidelberg (2003)
Jansson, P., Jeuring, J.: PolyP—a polytypic programming language extension. In: POPL 1997 (1997)
Licata, D.R., Harper, R.: A universe of binding and computation. In: ICFP 2009 (2009)
Martin-Löf, P.: Intuitionistic Type Theory. Bibliopolis (1984)
McBride, C., McKinna, J.: The view from the left. J. Funct. Program. 14(1), 69–111 (2004)
McKinna, J., Pollack, R.: Pure Type Systems Formalized. In: Bezem, M., Groote, J.F. (eds.) TLCA 1993. LNCS, vol. 664, pp. 289–305. Springer, Heidelberg (1993)
Momigliano, A., Martin, A.J., Felty, A.P.: Two-level hybrid: A system for reasoning using higher-order abstract syntax. Electron. Notes Theor. Comput. Sci. 196, 85–93 (2008)
Morris, P., Altenkirch, T., McBride, C.: Exploring the Regular Tree Types. In: Filliâtre, J.-C., Paulin-Mohring, C., Werner, B. (eds.) TYPES 2004. LNCS, vol. 3839, pp. 252–267. Springer, Heidelberg (2006)
Morris, P., Altenkirch, T., Ghani, N.: A universe of strictly positive families. Int. J. Found. Comput. Sci. 20(1), 83–107 (2009)
Nordström, B., Peterson, K., Smith, J.M.: Programming in Martin-Löf’s Type Theory: An Introduction. Oxford Unversity Press (1990)
Norell, U.: Towards a practical programming language based on dependent type theory. PhD thesis, Chalmers University of Technology (2007)
Norell, U.: Dependently Typed Programming in Agda. In: Koopman, P., Plasmeijer, R., Swierstra, D. (eds.) AFP 2008. LNCS, vol. 5832, pp. 230–266. Springer, Heidelberg (2009)
Paulin-Mohring, C.: Définitions Inductives en Théorie des Types d’Ordre Supérieur. Habilitation à diriger les recherches, Université Claude Bernard Lyon I (1996)
Peyton Jones, S., Vytiniotis, D., Weirich, S., Washburn, G.: Simple unification-based type inference for GADTs. In: ICFP 2006 (2006)
Pfenning, F., Elliot, C.: Higher-order abstract syntax. In: PLDI 1988 (1988)
Pfenning, F., Schürmann, C.: System Description: Twelf - A Meta-Logical Framework for Deductive Systems. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol. 1632, pp. 202–206. Springer, Heidelberg (1999)
Pierce, B.C.: Types and Programming Languages. The MIT Press (2002)
Pitts, A.M.: Nominal logic, a first order theory of names and binding. Inf. Comput. 186(2), 165–193 (2003)
Popescu, A., Gunter, E.L., Osborn, C.J.: Strong Normalization for System F by HOAS on top of FOAS. In: LICS, pp. 31–40 (2010)
Rodriguez, A., Jeuring, J., Jansson, P., Gerdes, A., Kiselyov, O., Oliveira, B.C.d.S.: Comparing libraries for generic programming in Haskell. In: Haskell 2008 (2008)
Rossberg, A., Russo, C.V., Dreyer, D.: F-ing modules. In: TLDI 2010 (2010)
Sato, M., Pollack, R.: External and internal syntax of the lambda-calculus. J. Symb. Comput. 45(5), 598–616 (2010)
Sewell, P., Nardelli, F.Z., Owens, S., Peskine, G., Ridge, T., Sarkar, S., Strniša, R.: Ott: Effective tool support for the working semanticist. J. Funct. Program. 20(01), 71–122 (2010)
Urban, C., Tasson, C.: Nominal Techniques in Isabelle/HOL. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol. 3632, pp. 38–53. Springer, Heidelberg (2005)
Verbruggen, W., de Vries, E., Hughes, A.: Polytypic programming in COQ. In: WGP 2008 (2008)
Verbruggen, W., de Vries, E., Hughes, A.: Polytypic properties and proofs in Coq. In: WGP 2009 (2009)
Vouillon, J.: Poplmark solutions using de bruijn indices (2007), https://alliance.seas.upenn.edu/~plclub/cgi-bin/poplmark/
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Lee, G., Oliveira, B.C.D.S., Cho, S., Yi, K. (2012). GMeta: A Generic Formal Metatheory Framework for First-Order Representations. In: Seidl, H. (eds) Programming Languages and Systems. ESOP 2012. Lecture Notes in Computer Science, vol 7211. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-28869-2_22
Download citation
DOI: https://doi.org/10.1007/978-3-642-28869-2_22
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-28868-5
Online ISBN: 978-3-642-28869-2
eBook Packages: Computer ScienceComputer Science (R0)