{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,30]],"date-time":"2026-03-30T02:30:31Z","timestamp":1774837831289,"version":"3.50.1"},"reference-count":18,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2011,5,3]],"date-time":"2011-05-03T00:00:00Z","timestamp":1304380800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2012,10]]},"DOI":"10.1007\/s10817-011-9226-1","type":"journal-article","created":{"date-parts":[[2011,5,2]],"date-time":"2011-05-02T10:44:49Z","timestamp":1304333089000},"page":"453-491","source":"Crossref","is-referenced-by-count":5,"title":["A List-Machine Benchmark for Mechanized Metatheory"],"prefix":"10.1007","volume":"49","author":[{"given":"Andrew W.","family":"Appel","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Robert","family":"Dockins","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xavier","family":"Leroy","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2011,5,3]]},"reference":[{"key":"9226_CR1","unstructured":"Appel, A.W.: Hints on Proving Theorems in Twelf (2000). http:\/\/www.cs.princeton.edu\/~appel\/twelf-tutorial"},{"key":"9226_CR2","unstructured":"Appel, A.W., Leroy, X.: List-Machine Exercise (2006). http:\/\/www.cs.princeton.edu\/~appel\/listmachine\/"},{"key":"9226_CR3","doi-asserted-by":"crossref","first-page":"109","DOI":"10.1145\/1190216.1190235","volume-title":"Proc. 34th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL\u201907)","author":"AW Appel","year":"2007","unstructured":"Appel, A.W., Melli\u00e8s, P.A., Richards, C.D., Vouillon, J.: A very modal model of a modern, major, general type system. In: Proc. 34th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL\u201907), pp. 109\u2013122. ACM, New York (2007)"},{"key":"9226_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"50","DOI":"10.1007\/11541868_4","volume-title":"Int. Conf. on Theorem Proving in Higher Order Logics (TPHOLs 2005)","author":"BE 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: Int. Conf. on Theorem Proving in Higher Order Logics (TPHOLs 2005), Lecture Notes in Computer Science, vol. 3603, pp. 50\u201365. Springer, Berlin (2005). http:\/\/plclub.org\/mmm\/"},{"key":"9226_CR5","series-title":"EATCS Texts in Theoretical Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-07964-5","volume-title":"Interactive Theorem Proving and Program Development\u2014Coq\u2019Art: The Calculus of Inductive Constructions","author":"Y Bertot","year":"2004","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development\u2014Coq\u2019Art: The Calculus of Inductive Constructions. EATCS Texts in Theoretical Computer Science. Springer, New York (2004)"},{"key":"9226_CR6","unstructured":"The Coq Proof Assistant (1984\u20132010). Software and documentation available from http:\/\/coq.inria.fr\/"},{"key":"9226_CR7","doi-asserted-by":"crossref","first-page":"131","DOI":"10.1145\/1411204.1411206","volume-title":"Proceeding of the 13th ACM SIGPLAN International Conference on Functional Programming, ICFP 2008","author":"O Danvy","year":"2008","unstructured":"Danvy, O.: Defunctionalized interpreters for programming languages. In: Proceeding of the 13th ACM SIGPLAN International Conference on Functional Programming, ICFP 2008, pp. 131\u2013142. ACM, New York (2008)"},{"key":"9226_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"70","DOI":"10.1007\/978-3-540-74591-4_7","volume-title":"Theorem Proving in Higher Order Logics (TPHOLs 2007)","author":"D Delahaye","year":"2007","unstructured":"Delahaye, D., Dubois, C., \u00c9tienne, J.F.: Extracting purely functional contents from logical inductive types. In: Theorem Proving in Higher Order Logics (TPHOLs 2007), Lecture Notes in Computer Science, vol. 4732, pp. 70\u201385. Springer, Berlin (2007)"},{"issue":"4","key":"9226_CR9","doi-asserted-by":"crossref","first-page":"619","DOI":"10.1145\/1146809.1146811","volume":"28","author":"G Klein","year":"2006","unstructured":"Klein, G., Nipkow, T.: A machine-checked model for a Java-like language, virtual machine and compiler. ACM Trans. Program. Lang. Syst. 28(4), 619\u2013695 (2006)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"9226_CR10","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1109\/SEFM.2005.51","volume-title":"3rd International Conference on Software Engineering and Formal Methods (SEFM 2005)","author":"D Leinenbach","year":"2005","unstructured":"Leinenbach, D., Paul, W., Petrova, E.: Towards the formal verification of a C0 compiler. In: 3rd International Conference on Software Engineering and Formal Methods (SEFM 2005), pp. 2\u201311. IEEE Computer Society, Los Alamitos (2005)"},{"issue":"7","key":"9226_CR11","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1145\/1538788.1538814","volume":"52","author":"X Leroy","year":"2009","unstructured":"Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107\u2013115 (2009)","journal-title":"Commun. ACM"},{"issue":"2","key":"9226_CR12","doi-asserted-by":"crossref","first-page":"284","DOI":"10.1016\/j.ic.2007.12.004","volume":"207","author":"X Leroy","year":"2009","unstructured":"Leroy, X., Grall, H.: Coinductive big-step operational semantics. Inf. Comput. 207(2), 284\u2013304 (2009)","journal-title":"Inf. Comput."},{"issue":"3","key":"9226_CR13","doi-asserted-by":"crossref","first-page":"528","DOI":"10.1145\/319301.319345","volume":"21","author":"G Morrisett","year":"1999","unstructured":"Morrisett, G., Walker, D., Crary, K., Glew, N.: From System F to typed assembly language. ACM Trans. Program. Lang. Syst. 21(3), 528\u2013569 (1999)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"9226_CR14","unstructured":"Pfenning, F., Schuermann, C.: Twelf User\u2019s Guide, Version 1.4 (2002). http:\/\/www.cs.cmu.edu\/~twelf\/guide-1-4"},{"key":"9226_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"202","DOI":"10.1007\/3-540-48660-7_14","volume-title":"CADE-16: Proceedings of the 16th International Conference on Automated Deduction","author":"F Pfenning","year":"1999","unstructured":"Pfenning, F., Sch\u00fcrmann, C.: System description: Twelf\u2014a meta-logical framework for deductive systems. In: CADE-16: Proceedings of the 16th International Conference on Automated Deduction, Lecture Notes in Computer Science, vol. 1632, pp.\u00a0202\u2013206. Springer, Berlin (1999)"},{"key":"9226_CR16","unstructured":"Weirich, S.: Experience Report with Twelf (2005). http:\/\/lists.seas.upenn.edu\/pipermail\/poplmark\/2005-August\/000220.html . E-mail to POPLmark mailing list, August 17"},{"issue":"1","key":"9226_CR17","doi-asserted-by":"crossref","first-page":"38","DOI":"10.1006\/inco.1994.1093","volume":"115","author":"AK Wright","year":"1994","unstructured":"Wright, A.K., Felleisen, M.: A syntactic approach to type soundness. Inf. Comput. 115(1), 38\u201394 (1994)","journal-title":"Inf. Comput."},{"key":"9226_CR18","doi-asserted-by":"crossref","first-page":"264","DOI":"10.1145\/888251.888276","volume-title":"5th ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming","author":"D Wu","year":"2003","unstructured":"Wu, D., Appel, A.W., Stump, A.: Foundational proof checkers with small witnesses. In: 5th ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming, pp. 264\u2013274. ACM, New York (2003)"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-011-9226-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-011-9226-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-011-9226-1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,31]],"date-time":"2019-05-31T01:21:51Z","timestamp":1559265711000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-011-9226-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,5,3]]},"references-count":18,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2012,10]]}},"alternative-id":["9226"],"URL":"https:\/\/doi.org\/10.1007\/s10817-011-9226-1","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011,5,3]]}}}