{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,24]],"date-time":"2025-09-24T10:33:24Z","timestamp":1758710004603},"publisher-location":"Berlin, Heidelberg","reference-count":45,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642288685"},{"type":"electronic","value":"9783642288692"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-28869-2_22","type":"book-chapter","created":{"date-parts":[[2012,3,22]],"date-time":"2012-03-22T20:44:36Z","timestamp":1332449076000},"page":"436-455","source":"Crossref","is-referenced-by-count":19,"title":["GMeta: A Generic Formal Metatheory Framework for First-Order Representations"],"prefix":"10.1007","author":[{"given":"Gyesik","family":"Lee","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bruno C. D. S.","family":"Oliveira","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sungkeun","family":"Cho","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kwangkeun","family":"Yi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"22_CR1","doi-asserted-by":"crossref","unstructured":"Altenkirch, T., McBride, C.: Generic programming within dependently typed programming. In: IFIP TC2\/WG2.1 Working Conference on Generic Programming (2003)","DOI":"10.1007\/978-0-387-35672-3_1"},{"key":"22_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1007\/3-540-48168-0_32","volume-title":"Computer Science Logic","author":"T. Altenkirch","year":"1999","unstructured":"Altenkirch, T., Reus, B.: Monadic Presentations of Lambda Terms Using Generalized Inductive Types. In: Flum, J., Rodr\u00edguez-Artalejo, M. (eds.) CSL 1999. LNCS, vol.\u00a01683, pp. 453\u2013468. Springer, Heidelberg (1999)"},{"key":"22_CR3","unstructured":"Aydemir, B., Weirich, S., Zdancewic, S.: Abstracting syntax. Technical Report MS-CIS-09-06, University of Pennsylvania (2009)"},{"key":"22_CR4","unstructured":"Aydemir, B.E., Weirich, S.: LNgen: Tool Support for Locally Nameless Representations (2009) (Unpublished manuscript)"},{"key":"22_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1007\/11541868_4","volume-title":"Theorem Proving in Higher Order Logics","author":"B.E. Aydemir","year":"2005","unstructured":"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.\u00a03603, pp. 50\u201365. Springer, Heidelberg (2005)"},{"key":"22_CR6","doi-asserted-by":"crossref","unstructured":"Aydemir, B.E., Chargu\u00e9raud, A., Pierce, B.C., Pollack, R., Weirich, S.: Engineering formal metatheory. In: POPL 2008 (2008)","DOI":"10.1145\/1328438.1328443"},{"key":"22_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"515","DOI":"10.1007\/BFb0014565","volume-title":"Theoretical Aspects of Computer Software","author":"S. Boutin","year":"1997","unstructured":"Boutin, S.: Using Reflection to Build Efficient and Certified Decision Procedures. In: Ito, T., Abadi, M. (eds.) TACS 1997. LNCS, vol.\u00a01281, pp. 515\u2013529. Springer, Heidelberg (1997)"},{"key":"22_CR8","doi-asserted-by":"crossref","unstructured":"Cheney, J.: Scrap your nameplate (functional pearl). In: ICFP 2005 (2005)","DOI":"10.1145\/1086365.1086389"},{"key":"22_CR9","doi-asserted-by":"crossref","unstructured":"Chlipala, A.: A certified type-preserving compiler from lambda calculus to assembly language. In: PLDI 2007 (2007)","DOI":"10.1145\/1250734.1250742"},{"key":"22_CR10","doi-asserted-by":"crossref","unstructured":"Chlipala, A.: Parametric higher-order abstract syntax for mechanized semantics. In: ICFP 2008 (2008)","DOI":"10.1145\/1411204.1411226"},{"key":"22_CR11","unstructured":"The Coq Development\u00a0Team. The Coq Proof Assistant Reference Manual, Version 8.2 (2009), \n                  \n                    http:\/\/coq.inria.fr"},{"issue":"5","key":"22_CR12","doi-asserted-by":"publisher","first-page":"381","DOI":"10.1016\/1385-7258(72)90034-0","volume":"75","author":"N.G. Bruijn de","year":"1972","unstructured":"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)\u00a075(5), 381\u2013392 (1972)","journal-title":"Indagationes Mathematicae (Proceedings)"},{"key":"22_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"124","DOI":"10.1007\/BFb0014049","volume-title":"Typed Lambda Calculi and Applications","author":"J. Despeyroux","year":"1995","unstructured":"Despeyroux, J., Felty, A.P., Hirschowitz, A.: Higher-Order Abstract Syntax in Coq. In: Dezani-Ciancaglini, M., Plotkin, G. (eds.) TLCA 1995. LNCS, vol.\u00a0902, pp. 124\u2013138. Springer, Heidelberg (1995)"},{"key":"22_CR14","doi-asserted-by":"publisher","first-page":"440","DOI":"10.1007\/BF01211308","volume":"6","author":"P. Dybjer","year":"1997","unstructured":"Dybjer, P.: Inductive families. Formal Aspects of Computing\u00a06, 440\u2013465 (1997)","journal-title":"Formal Aspects of Computing"},{"key":"22_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1007\/3-540-48959-2_11","volume-title":"Typed Lambda Calculi and Applications","author":"P. Dybjer","year":"1999","unstructured":"Dybjer, P., Setzer, A.: A Finite Axiomatization of Inductive-Recursive Definitions. In: Girard, J.-Y. (ed.) TLCA 1999. LNCS, vol.\u00a01581, pp. 129\u2013146. Springer, Heidelberg (1999)"},{"key":"22_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/3-540-45504-3_7","volume-title":"Proof Theory in Computer Science","author":"P. Dybjer","year":"2001","unstructured":"Dybjer, P., Setzer, A.: Indexed Induction-Recursion. In: Kahle, R., Schroeder-Heister, P., St\u00e4rk, R.F. (eds.) PTCS 2001. LNCS, vol.\u00a02183, pp. 93\u2013113. Springer, Heidelberg (2001)"},{"key":"22_CR17","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/978-3-540-71070-7_13","volume-title":"Automated Reasoning","author":"A. Gacek","year":"2008","unstructured":"Gacek, A.: The Abella Interactive Theorem Prover (System Description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol.\u00a05195, pp. 154\u2013161. Springer, Heidelberg (2008)"},{"issue":"1","key":"22_CR18","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1145\/138027.138060","volume":"40","author":"R. Harper","year":"1993","unstructured":"Harper, R., Honsell, F., Plotkin, G.: A framework for defining logics. J. ACM\u00a040(1), 143\u2013184 (1993)","journal-title":"J. ACM"},{"key":"22_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-45191-4_1","volume-title":"Generic Programming","author":"R. Hinze","year":"2003","unstructured":"Hinze, R., Jeuring, J.: Generic Haskell: Practice and Theory. In: Backhouse, R., Gibbons, J. (eds.) Generic Programming SS 2002. LNCS, vol.\u00a02793, pp. 1\u201356. Springer, Heidelberg (2003)"},{"key":"22_CR20","doi-asserted-by":"crossref","unstructured":"Jansson, P., Jeuring, J.: PolyP\u2014a polytypic programming language extension. In: POPL 1997 (1997)","DOI":"10.1145\/263699.263763"},{"key":"22_CR21","doi-asserted-by":"crossref","unstructured":"Licata, D.R., Harper, R.: A universe of binding and computation. In: ICFP 2009 (2009)","DOI":"10.1145\/1596550.1596571"},{"key":"22_CR22","unstructured":"Martin-L\u00f6f, P.: Intuitionistic Type Theory. Bibliopolis (1984)"},{"issue":"1","key":"22_CR23","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1017\/S0956796803004829","volume":"14","author":"C. McBride","year":"2004","unstructured":"McBride, C., McKinna, J.: The view from the left. J. Funct. Program.\u00a014(1), 69\u2013111 (2004)","journal-title":"J. Funct. Program."},{"key":"22_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"289","DOI":"10.1007\/BFb0037113","volume-title":"Typed Lambda Calculi and Applications","author":"J. McKinna","year":"1993","unstructured":"McKinna, J., Pollack, R.: Pure Type Systems Formalized. In: Bezem, M., Groote, J.F. (eds.) TLCA 1993. LNCS, vol.\u00a0664, pp. 289\u2013305. Springer, Heidelberg (1993)"},{"key":"22_CR25","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1016\/j.entcs.2007.09.019","volume":"196","author":"A. Momigliano","year":"2008","unstructured":"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.\u00a0196, 85\u201393 (2008)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"22_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"252","DOI":"10.1007\/11617990_16","volume-title":"Types for Proofs and Programs","author":"P. Morris","year":"2006","unstructured":"Morris, P., Altenkirch, T., McBride, C.: Exploring the Regular Tree Types. In: Filli\u00e2tre, J.-C., Paulin-Mohring, C., Werner, B. (eds.) TYPES 2004. LNCS, vol.\u00a03839, pp. 252\u2013267. Springer, Heidelberg (2006)"},{"issue":"1","key":"22_CR27","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1142\/S0129054109006462","volume":"20","author":"P. Morris","year":"2009","unstructured":"Morris, P., Altenkirch, T., Ghani, N.: A universe of strictly positive families. Int. J. Found. Comput. Sci.\u00a020(1), 83\u2013107 (2009)","journal-title":"Int. J. Found. Comput. Sci."},{"key":"22_CR28","unstructured":"Nordstr\u00f6m, B., Peterson, K., Smith, J.M.: Programming in Martin-L\u00f6f\u2019s Type Theory: An Introduction. Oxford Unversity Press (1990)"},{"key":"22_CR29","unstructured":"Norell, U.: Towards a practical programming language based on dependent type theory. PhD thesis, Chalmers University of Technology (2007)"},{"key":"22_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"230","DOI":"10.1007\/978-3-642-04652-0_5","volume-title":"Advanced Functional Programming","author":"U. Norell","year":"2009","unstructured":"Norell, U.: Dependently Typed Programming in Agda. In: Koopman, P., Plasmeijer, R., Swierstra, D. (eds.) AFP 2008. LNCS, vol.\u00a05832, pp. 230\u2013266. Springer, Heidelberg (2009)"},{"key":"22_CR31","unstructured":"Paulin-Mohring, C.: D\u00e9finitions Inductives en Th\u00e9orie des Types d\u2019Ordre Sup\u00e9rieur. Habilitation \u00e0 diriger les recherches, Universit\u00e9 Claude Bernard Lyon I (1996)"},{"key":"22_CR32","doi-asserted-by":"crossref","unstructured":"Peyton Jones, S., Vytiniotis, D., Weirich, S., Washburn, G.: Simple unification-based type inference for GADTs. In: ICFP 2006 (2006)","DOI":"10.1145\/1159803.1159811"},{"key":"22_CR33","doi-asserted-by":"crossref","unstructured":"Pfenning, F., Elliot, C.: Higher-order abstract syntax. In: PLDI 1988 (1988)","DOI":"10.1145\/53990.54010"},{"key":"22_CR34","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"202","DOI":"10.1007\/3-540-48660-7_14","volume-title":"Automated Deduction - CADE-16","author":"F. Pfenning","year":"1999","unstructured":"Pfenning, F., Sch\u00fcrmann, C.: System Description: Twelf - A Meta-Logical Framework for Deductive Systems. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol.\u00a01632, pp. 202\u2013206. Springer, Heidelberg (1999)"},{"key":"22_CR35","unstructured":"Pierce, B.C.: Types and Programming Languages. The MIT Press (2002)"},{"issue":"2","key":"22_CR36","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1016\/S0890-5401(03)00138-X","volume":"186","author":"A.M. Pitts","year":"2003","unstructured":"Pitts, A.M.: Nominal logic, a first order theory of names and binding. Inf. Comput.\u00a0186(2), 165\u2013193 (2003)","journal-title":"Inf. Comput."},{"key":"22_CR37","doi-asserted-by":"crossref","unstructured":"Popescu, A., Gunter, E.L., Osborn, C.J.: Strong Normalization for System F by HOAS on top of FOAS. In: LICS, pp. 31\u201340 (2010)","DOI":"10.1109\/LICS.2010.48"},{"key":"22_CR38","doi-asserted-by":"crossref","unstructured":"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)","DOI":"10.1145\/1411286.1411301"},{"key":"22_CR39","doi-asserted-by":"crossref","unstructured":"Rossberg, A., Russo, C.V., Dreyer, D.: F-ing modules. In: TLDI 2010 (2010)","DOI":"10.1145\/1708016.1708028"},{"issue":"5","key":"22_CR40","doi-asserted-by":"publisher","first-page":"598","DOI":"10.1016\/j.jsc.2010.01.010","volume":"45","author":"M. Sato","year":"2010","unstructured":"Sato, M., Pollack, R.: External and internal syntax of the lambda-calculus. J. Symb. Comput.\u00a045(5), 598\u2013616 (2010)","journal-title":"J. Symb. Comput."},{"issue":"01","key":"22_CR41","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1017\/S0956796809990293","volume":"20","author":"P. Sewell","year":"2010","unstructured":"Sewell, P., Nardelli, F.Z., Owens, S., Peskine, G., Ridge, T., Sarkar, S., Strni\u0161a, R.: Ott: Effective tool support for the working semanticist. J. Funct. Program.\u00a020(01), 71\u2013122 (2010)","journal-title":"J. Funct. Program."},{"key":"22_CR42","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1007\/11532231_4","volume-title":"Automated Deduction \u2013 CADE-20","author":"C. Urban","year":"2005","unstructured":"Urban, C., Tasson, C.: Nominal Techniques in Isabelle\/HOL. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol.\u00a03632, pp. 38\u201353. Springer, Heidelberg (2005)"},{"key":"22_CR43","doi-asserted-by":"crossref","unstructured":"Verbruggen, W., de Vries, E., Hughes, A.: Polytypic programming in COQ. In: WGP 2008 (2008)","DOI":"10.1145\/1411318.1411326"},{"key":"22_CR44","doi-asserted-by":"crossref","unstructured":"Verbruggen, W., de Vries, E., Hughes, A.: Polytypic properties and proofs in Coq. In: WGP 2009 (2009)","DOI":"10.1145\/1596614.1596616"},{"key":"22_CR45","unstructured":"Vouillon, J.: Poplmark solutions using de bruijn indices (2007), \n                  \n                    https:\/\/alliance.seas.upenn.edu\/~plclub\/cgi-bin\/poplmark\/"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-28869-2_22.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,4]],"date-time":"2021-05-04T11:13:41Z","timestamp":1620126821000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-28869-2_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642288685","9783642288692"],"references-count":45,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-28869-2_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}