{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T23:11:12Z","timestamp":1784848272262,"version":"3.55.0"},"publisher-location":"New York, NY, USA","reference-count":51,"publisher":"ACM","license":[{"start":{"date-parts":[[2008,1,7]],"date-time":"2008-01-07T00:00:00Z","timestamp":1199664000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2008,1,7]]},"DOI":"10.1145\/1328438.1328443","type":"proceedings-article","created":{"date-parts":[[2008,1,7]],"date-time":"2008-01-07T09:45:40Z","timestamp":1199699140000},"page":"3-15","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":112,"title":["Engineering formal metatheory"],"prefix":"10.1145","author":[{"given":"Brian","family":"Aydemir","sequence":"first","affiliation":[{"name":"University of Pennsylvania, Philadelphia, PA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Arthur","family":"Chargu\u00e9raud","sequence":"additional","affiliation":[{"name":"INRIA, Rocquencourt, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Benjamin C.","family":"Pierce","sequence":"additional","affiliation":[{"name":"University of Pennsylvania, Philadelphia, PA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Randy","family":"Pollack","sequence":"additional","affiliation":[{"name":"University of Edinburgh, Edinburgh, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Stephanie","family":"Weirich","sequence":"additional","affiliation":[{"name":"University of Pennsylvania, Philadelphia, PA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2008,1,7]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.5555\/645891.671436"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.5555\/871816.871860"},{"key":"e_1_3_2_1_3_1","volume-title":"Submission to the POPLMARK challenge. Available from http:\/\/www.cis.upenn.edu\/~plclub\/mmm\/","author":"Ashley-Rollman Michael","year":"2005","unstructured":"Michael Ashley-Rollman , Karl Crary , and Robert Harper . Submission to the POPLMARK challenge. Available from http:\/\/www.cis.upenn.edu\/~plclub\/mmm\/ , 2005 . Michael Ashley-Rollman, Karl Crary, and Robert Harper. Submission to the POPLMARK challenge. Available from http:\/\/www.cis.upenn.edu\/~plclub\/mmm\/, 2005."},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/11541868_4"},{"key":"e_1_3_2_1_5_1","volume-title":"The Lambda Calculus. North Holland, revised edition","author":"Barendregt Henk P.","year":"1984","unstructured":"Henk P. Barendregt . The Lambda Calculus. North Holland, revised edition , 1984 . Henk P. Barendregt. The Lambda Calculus. North Holland, revised edition, 1984."},{"key":"e_1_3_2_1_6_1","volume-title":"Coq in coq. Available from http:\/\/pauillac.inria.fr\/~barras\/coq_work-eng.html","author":"Barras Bruno","year":"1997","unstructured":"Bruno Barras and Benjamin Werner . Coq in coq. Available from http:\/\/pauillac.inria.fr\/~barras\/coq_work-eng.html , 1997 . Bruno Barras and Benjamin Werner. Coq in coq. Available from http:\/\/pauillac.inria.fr\/~barras\/coq_work-eng.html, 1997."},{"key":"e_1_3_2_1_7_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0037093","volume-title":"TLCA'93","author":"Bezem M.","year":"1993","unstructured":"M. Bezem and J. F. Groote , editors . Typed Lambda Calculi and Applications: International Conference on Typed Lambda Calculi and Applications , TLCA'93 , volume 664 of Lecture Notes in Computer Science , 1993 . Springer . M. Bezem and J. F. Groote, editors. Typed Lambda Calculi and Applications: International Conference on Typed Lambda Calculi and Applications, TLCA'93, volume 664 of Lecture Notes in Computer Science, 1993. Springer."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796806005892"},{"key":"e_1_3_2_1_9_1","volume-title":"Submission to the POPLMARK challenge, part 1a. Available from http:\/\/www.cs.berkeley.edu\/~adamc\/poplmark\/","author":"Chlipala Adam","year":"2006","unstructured":"Adam Chlipala . Submission to the POPLMARK challenge, part 1a. Available from http:\/\/www.cs.berkeley.edu\/~adamc\/poplmark\/ , 2006 . Adam Chlipala. Submission to the POPLMARK challenge, part 1a. Available from http:\/\/www.cs.berkeley.edu\/~adamc\/poplmark\/, 2006."},{"key":"e_1_3_2_1_10_1","volume-title":"The Coq proof assistant reference manual, version 8.1. Available from http:\/\/coq.inria.fr\/","author":"Development Team The Coq","year":"2007","unstructured":"The Coq Development Team . The Coq proof assistant reference manual, version 8.1. Available from http:\/\/coq.inria.fr\/ , 2007 . The Coq Development Team. The Coq proof assistant reference manual, version 8.1. Available from http:\/\/coq.inria.fr\/, 2007."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.5555\/120477.120486"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/604131.604149"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1016\/1385-7258(72)90034-0"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.5555\/645892.671587"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01211308"},{"key":"e_1_3_2_1_16_1","first-page":"42","article-title":"Operational techniques in PVS - A preliminary evaluation","author":"Ford Jonathan M.","year":"2001","unstructured":"Jonathan M. Ford and Ian A. Mason . Operational techniques in PVS - A preliminary evaluation . Electronic Notes in Theoretical Computer Science , 42 , 2001 . Jonathan M. Ford and Ian A. Mason. Operational techniques in PVS - A preliminary evaluation. Electronic Notes in Theoretical Computer Science, 42, 2001.","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"e_1_3_2_1_17_1","volume-title":"North-Holland","author":"Gentzen Gerhard","year":"1969","unstructured":"Gerhard Gentzen . The Collected Papers of Gerhard Gentzen . North-Holland , 1969 . Edited by Mandred Szabo. Gerhard Gentzen. The Collected Papers of Gerhard Gentzen. North-Holland, 1969. Edited by Mandred Szabo."},{"key":"e_1_3_2_1_18_1","series-title":"Lecture Notes in Computer Science","first-page":"414","volume-title":"J. J. Joyce and C.-J","author":"Gordon Andrew D.","year":"1993","unstructured":"Andrew D. Gordon . A mechanisation of name-carrying syntax up to alphaconversion . In J. J. Joyce and C.-J . H. Seger, editors, Higher-order Logic Theorem Proving And Its Applications, Proceedings , 1993 , volume 780 of Lecture Notes in Computer Science , pages 414 -- 426 . Springer , 1994. Andrew D. Gordon. A mechanisation of name-carrying syntax up to alphaconversion. In J. J. Joyce and C.-J. H. Seger, editors, Higher-order Logic Theorem Proving And Its Applications, Proceedings, 1993, volume 780 of Lecture Notes in Computer Science, pages 414--426. Springer, 1994."},{"key":"e_1_3_2_1_19_1","series-title":"Lecture Notes in Computer Science","first-page":"173","volume-title":"Theorem Proving in Higher Order Logics: 9th International Conference, TPHOLs'96","author":"Andrew","year":"1996","unstructured":"Andrew D. Gordon and Tom Melham. Five axioms of alpha-conversion . In J. von Wright, J. Grundy, and J. Harrison, editors, Theorem Proving in Higher Order Logics: 9th International Conference, TPHOLs'96 , volume 1125 of Lecture Notes in Computer Science , pages 173 -- 190 . Springer , 1996 . Andrew D. Gordon and Tom Melham. Five axioms of alpha-conversion. In J. von Wright, J. Grundy, and J. Harrison, editors, Theorem Proving in Higher Order Logics: 9th International Conference, TPHOLs'96, volume 1125 of Lecture Notes in Computer Science, pages 173--190. Springer, 1996."},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796807006430"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/138027.138060"},{"key":"e_1_3_2_1_22_1","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"136","DOI":"10.1007\/978-3-540-45085-6_11","volume-title":"Automated Deduction - CADE-19","author":"Hendriks Dimitri","year":"2003","unstructured":"Dimitri Hendriks and Vincent van Oostrom . Adbmal . In F. Baader, editor, Automated Deduction - CADE-19 , volume 2741 of Lecture Notes in Artificial Intelligence , pages 136 -- 150 . Springer-Verlag , 2003 . Dimitri Hendriks and Vincent van Oostrom. Adbmal. In F. Baader, editor, Automated Deduction - CADE-19, volume 2741 of Lecture Notes in Artificial Intelligence, pages 136--150. Springer-Verlag, 2003."},{"key":"e_1_3_2_1_23_1","first-page":"207","volume-title":"A proof of the Church-Rosser theorem for the lambda calculus in higher order logic","author":"Homeier Peter","year":"2001","unstructured":"Peter Homeier . A proof of the Church-Rosser theorem for the lambda calculus in higher order logic . In Richard J. Boulton and Paul B. Jackson, editors, TPHOLs 2001 : Supplemental Proceedings, pages 207 -- 222 . Division of Informatics, University of Edinburgh , September 2001. Available as Informatics Research Report EDI-INF-RR-0046. Peter Homeier. A proof of the Church-Rosser theorem for the lambda calculus in higher order logic. In Richard J. Boulton and Paul B. Jackson, editors, TPHOLs 2001: Supplemental Proceedings, pages 207--222. Division of Informatics, University of Edinburgh, September 2001. Available as Informatics Research Report EDI-INF-RR-0046."},{"key":"e_1_3_2_1_24_1","first-page":"62","article-title":"The theory of contexts for first order and higher order abstract syntax","author":"Honsell Furio","year":"2002","unstructured":"Furio Honsell , Marino Miculan , and Ivan Scagnetto . The theory of contexts for first order and higher order abstract syntax . Electronic Notes in Theoretical Computer Science , 62 , 2002 . Furio Honsell, Marino Miculan, and Ivan Scagnetto. The theory of contexts for first order and higher order abstract syntax. Electronic Notes in Theoretical Computer Science, 62, 2002.","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"e_1_3_2_1_25_1","volume-title":"The constructive engine","author":"Huet G\u00e9rard","year":"1989","unstructured":"G\u00e9rard Huet . The constructive engine . In Raghavan Narasimhan, editor, A Perspective in Theoretical Computer Science: Commerative Volume for Gift Siromoney. World Scientific Publishing , 1989 . Also available as INRIA Technical Report 110. G\u00e9rard Huet. The constructive engine. In Raghavan Narasimhan, editor, A Perspective in Theoretical Computer Science: Commerative Volume for Gift Siromoney. World Scientific Publishing, 1989. Also available as INRIA Technical Report 110."},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796800001106"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/1146809.1146811"},{"key":"e_1_3_2_1_28_1","unstructured":"J. L. Krivine. Lambda-Calculus Types and Models. Ellis Horwood 1990.   J. L. Krivine. Lambda-Calculus Types and Models. Ellis Horwood 1990."},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190245"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111042"},{"key":"e_1_3_2_1_31_1","volume-title":"INRIA","author":"Leroy Xavier","year":"2007","unstructured":"Xavier Leroy . A locally nameless solution to the POPLmark challenge. Research report 6098 , INRIA , January 2007 . Xavier Leroy. A locally nameless solution to the POPLmark challenge. Research report 6098, INRIA, January 2007."},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/1017472.1017477"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.5555\/645891.756642"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1006294005493"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1006496715975"},{"key":"e_1_3_2_1_37_1","volume-title":"Available from http:\/\/hol.sourceforge.net\/","author":"Norrish Michael","year":"2007","unstructured":"Michael Norrish and Konrad Slind . HOL 4. Available from http:\/\/hol.sourceforge.net\/ , 2007 . Michael Norrish and Konrad Slind. HOL 4. Available from http:\/\/hol.sourceforge.net\/, 2007."},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/53990.54010"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"crossref","unstructured":"Frank\n      Pfenning\n     and \n      Carsten\n      Sch\u00fcrmann\n    .\n  System description: Twelf - A meta-logical framework for deductive systems\n  . In Harald Ganzinger editor Automated Deduction CADE 16:  16th International Conference on Automated Deduction volume \n  1632\n   of \n  Lecture Notes in Artificial Intelligence pages \n  202\n  --\n  206\n  . \n  Springer 1999\n  .   Frank Pfenning and Carsten Sch\u00fcrmann. System description: Twelf - A meta-logical framework for deductive systems. In Harald Ganzinger editor Automated Deduction CADE 16: 16th International Conference on Automated Deduction volume 1632 of Lecture Notes in Artificial Intelligence pages 202--206. Springer 1999.","DOI":"10.1007\/3-540-48660-7_14"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0890-5401(03)00138-X"},{"key":"e_1_3_2_1_41_1","volume-title":"February","author":"Pollack Randy","year":"2006","unstructured":"Randy Pollack . Reasoning about languages with binding: Can we do it yet? , February 2006 . Presentation , slides available from http:\/\/homepages.inf.ed.ac.uk\/rpollack\/. Randy Pollack. Reasoning about languages with binding: Can we do it yet?, February 2006. Presentation, slides available from http:\/\/homepages.inf.ed.ac.uk\/rpollack\/."},{"key":"e_1_3_2_1_42_1","unstructured":"Robert\n      Pollack\n    .\n  Closure under alpha-conversion\n  . In H. Barendregt and T. Nipkow editors TYPES'93: Workshop on Types for Proofs and Programs Nijmegen May \n  1993 Selected Papers volume \n  806\n   of \n  Lecture Notes in Computer Science pages \n  313\n  --\n  332\n  . \n  Springer 1994a.   Robert Pollack. Closure under alpha-conversion. In H. Barendregt and T. Nipkow editors TYPES'93: Workshop on Types for Proofs and Programs Nijmegen May 1993 Selected Papers volume 806 of Lecture Notes in Computer Science pages 313--332. Springer 1994a."},{"key":"e_1_3_2_1_44_1","volume-title":"Almquist and Wiksell","author":"Prawitz Dag","year":"1965","unstructured":"Dag Prawitz . Natural Deduction : Proof Theoretical Study . Almquist and Wiksell , Stockholm , 1965 . Dag Prawitz. Natural Deduction: Proof Theoretical Study. Almquist and Wiksell, Stockholm, 1965."},{"key":"e_1_3_2_1_46_1","volume-title":"Submission to the POPLMARK challenge, part 1a. Available from http:\/\/ricciott.web.cs.unibo.it\/","author":"Ricciotti Wilmer","year":"2007","unstructured":"Wilmer Ricciotti . Submission to the POPLMARK challenge, part 1a. Available from http:\/\/ricciott.web.cs.unibo.it\/ , 2007 . Wilmer Ricciotti. Submission to the POPLMARK challenge, part 1a. Available from http:\/\/ricciott.web.cs.unibo.it\/, 2007."},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/1291151.1291155"},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/44483.44484"},{"key":"e_1_3_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(88)90149-1"},{"key":"e_1_3_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-008-9097-2"},{"key":"e_1_3_2_1_51_1","volume-title":"Locally nameless representation in Nominal Isabelle. Talk at Workshop on Mechanizing Metatheory. Available from www4.in.tum.de\/~urbanc\/Publications\/ln.pdf","author":"Urban Christian","year":"2007","unstructured":"Christian Urban and Randy Pollack . Locally nameless representation in Nominal Isabelle. Talk at Workshop on Mechanizing Metatheory. Available from www4.in.tum.de\/~urbanc\/Publications\/ln.pdf , 2007 . Christian Urban and Randy Pollack. Locally nameless representation in Nominal Isabelle. Talk at Workshop on Mechanizing Metatheory. Available from www4.in.tum.de\/~urbanc\/Publications\/ln.pdf, 2007."},{"key":"e_1_3_2_1_52_1","volume-title":"Nominal datatype package for Isabelle\/HOL. Available from http:\/\/isabelle.in.tum.de\/nominal\/","author":"Urban Christian","year":"2007","unstructured":"Christian Urban , Stefan Berghofer , and Julien Narboux . Nominal datatype package for Isabelle\/HOL. Available from http:\/\/isabelle.in.tum.de\/nominal\/ , 2007 a. Christian Urban, Stefan Berghofer, and Julien Narboux. Nominal datatype package for Isabelle\/HOL. Available from http:\/\/isabelle.in.tum.de\/nominal\/, 2007a."},{"key":"e_1_3_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73595-3_4"},{"key":"e_1_3_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0890-5401(03)00023-3"}],"event":{"name":"POPL08: The 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","location":"San Francisco California USA","acronym":"POPL08","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","ACM Association for Computing Machinery","SIGACT ACM Special Interest Group on Algorithms and Computation Theory"]},"container-title":["Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1328438.1328443","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1328438.1328443","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T09:56:07Z","timestamp":1750240567000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1328438.1328443"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,1,7]]},"references-count":51,"alternative-id":["10.1145\/1328438.1328443","10.1145\/1328438"],"URL":"https:\/\/doi.org\/10.1145\/1328438.1328443","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/1328897.1328443","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2008,1,7]]},"assertion":[{"value":"2008-01-07","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}