{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,10]],"date-time":"2026-04-10T03:12:21Z","timestamp":1775790741097,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":36,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540283720","type":"print"},{"value":"9783540318200","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11541868_4","type":"book-chapter","created":{"date-parts":[[2010,7,20]],"date-time":"2010-07-20T19:12:52Z","timestamp":1279653172000},"page":"50-65","source":"Crossref","is-referenced-by-count":188,"title":["Mechanized Metatheory for the Masses: The PoplMark Challenge"],"prefix":"10.1007","author":[{"given":"Brian E.","family":"Aydemir","sequence":"first","affiliation":[]},{"given":"Aaron","family":"Bohannon","sequence":"additional","affiliation":[]},{"given":"Matthew","family":"Fairbairn","sequence":"additional","affiliation":[]},{"given":"J. Nathan","family":"Foster","sequence":"additional","affiliation":[]},{"given":"Benjamin C.","family":"Pierce","sequence":"additional","affiliation":[]},{"given":"Peter","family":"Sewell","sequence":"additional","affiliation":[]},{"given":"Dimitrios","family":"Vytiniotis","sequence":"additional","affiliation":[]},{"given":"Geoffrey","family":"Washburn","sequence":"additional","affiliation":[]},{"given":"Stephanie","family":"Weirich","sequence":"additional","affiliation":[]},{"given":"Steve","family":"Zdancewic","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"4_CR1","doi-asserted-by":"crossref","unstructured":"Appel, A.W.: Foundational proof-carrying code. In: IEEE Symposium on Logic in Computer Science (LICS), Boston, Massachusetts, June 2001, pp. 247\u2013258 (2001)","DOI":"10.1109\/LICS.2001.932501"},{"key":"4_CR2","volume-title":"Theoretical Aspects of Object-Oriented Programming: Types, Semantics, and Language Design","author":"L. Cardelli","year":"1994","unstructured":"Cardelli, L.: Extensible records in a pure calculus of subtyping. Research report\u00a081, DEC\/Compaq Systems Research Center (January 1992) Also In: Gunter, C.A., Mitchell, J.C. (eds.) Theoretical Aspects of Object-Oriented Programming: Types, Semantics, and Language Design. MIT Press, Cambridge (1994)"},{"issue":"1\u20132","key":"4_CR3","doi-asserted-by":"publisher","first-page":"4","DOI":"10.1006\/inco.1994.1013","volume":"109","author":"L. Cardelli","year":"1994","unstructured":"Cardelli, L., Martini, S., Mitchell, J.C., Scedrov, A.: An extension of System F with subtyping. Information and Computation\u00a0109(1\u20132), 4\u201356 (1994); Summary in TACS 1991 (Sendai, Japan, pp.\u00a0750\u2013770) (1991)","journal-title":"Information and Computation"},{"key":"4_CR4","doi-asserted-by":"crossref","unstructured":"Crary, K.: Toward a foundational typed assembly language. In: ACM SIGPLAN\u2013SIGACT Symposium on Principles of Programming Languages (POPL), New Orleans, Louisiana, January 2003, pp. 198\u2013212 (2003)","DOI":"10.1145\/604131.604149"},{"key":"4_CR5","unstructured":"Dennis, L.A.: Inductive challenge problems (2000), http:\/\/www.cs.nott.ac.uk\/~lad\/research\/challenges"},{"issue":"3-4","key":"4_CR6","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1023\/A:1006285817788","volume":"23","author":"C. Dubois","year":"1999","unstructured":"Dubois, C., Menissier-Morain, V.: Certification of a type inference tool for ML: Damas-Milner within Coq. Journal of Automated Reasoning\u00a023(3-4), 319\u2013346 (1999)","journal-title":"Journal of Automated Reasoning"},{"key":"4_CR7","series-title":"Mathematical Aspects of Computer Science","first-page":"19","volume-title":"Proceedings of Symposia in Applied Mathematics","author":"R.W. Floyd","year":"1967","unstructured":"Floyd, R.W.: Assigning meanings to programs. In: Schwartz, J.T. (ed.) Proceedings of Symposia in Applied Mathematics. Mathematical Aspects of Computer Science, vol.\u00a019, pp. 19\u201332. American Mathematical Society, Providence (1967)"},{"key":"4_CR8","doi-asserted-by":"crossref","unstructured":"Gabbay, M., Pitts, A.: A new approach to abstract syntax involving binders. In: 14th Symposium on Logic in Computer Science, pp. 214\u2013224 (1999)","DOI":"10.1109\/LICS.1999.782617"},{"key":"4_CR9","doi-asserted-by":"crossref","unstructured":"Gent, I.P., Walsh, T.: CSPLib: a benchmark library for constraints. Technical Report APES-09-1999, APES. A shorter version appears in the Proceedings of the 5th International Conference on Principles and Practices of Constraint Programming, CP-99 (1999), Available from http:\/\/www.dcs.st-and.ac.uk\/~apes\/apesreports.html","DOI":"10.1007\/978-3-540-48085-3_36"},{"key":"4_CR10","unstructured":"Ghelli, G.: Proof Theoretic Studies about a Minimal Type System Integrating Inclusion and Parametric Polymorphism. PhD thesis, Universit\u00e0 di Pisa, Technical report TD\u20136\/90, Dipartimento di Informatica, Universit\u00e0 di Pisa (1990)"},{"key":"4_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"173","DOI":"10.1007\/BFb0105404","volume-title":"Theorem Proving in Higher Order Logics","author":"A.D. Gordon","year":"1996","unstructured":"Gordon, A.D., Melham, T.: Five axioms of alpha-conversion. In: von Wright, J., Harrison, J., Grundy, J. (eds.) TPHOLs 1996. LNCS, vol.\u00a01125, pp. 173\u2013190. Springer, Heidelberg (1996)"},{"key":"4_CR12","unstructured":"Green, I.: The dream corpus of inductive conjectures (1999), http:\/\/dream.dai.ed.ac.uk\/dc\/lib.html"},{"issue":"2","key":"4_CR13","doi-asserted-by":"crossref","first-page":"142","DOI":"10.1093\/comjnl\/38.2.142","volume":"38","author":"E. Gunter","year":"1995","unstructured":"Gunter, E., Maharaj, S.: Studying the ML module system in HOL. The Computer Journal: Special Issue on Theorem Proving in Higher Order Logics\u00a038(2), 142\u2013151 (1995)","journal-title":"The Computer Journal: Special Issue on Theorem Proving in Higher Order Logics"},{"issue":"1","key":"4_CR14","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1145\/602382.602403","volume":"50","author":"T. Hoare","year":"2003","unstructured":"Hoare, T.: The verifying compiler: A grand challenge for computing research. J. ACM\u00a050(1), 63\u201369 (2003)","journal-title":"J. ACM"},{"key":"4_CR15","unstructured":"Hoos, H., Stuetzle, T.: SATLIB., http:\/\/www.intellektik.informatik.tu-darmstadt.de\/SATLIB\/"},{"key":"4_CR16","series-title":"Lecture Notes in Computer Science","volume-title":"Higher Order Logic Theorem Proving and Its Applications","year":"1994","unstructured":"Joyce, J.J., Seger, C.-J.H. (eds.): HUG 1993. LNCS, vol.\u00a0780. Springer, Heidelberg (1994)"},{"key":"4_CR17","unstructured":"Klein, G., Nipkow, T.: A machine-checked model for a Java-like language, virtual machine and compiler. Technical Report 0400001T.1, National ICT Australia, Sydney (March 2004)"},{"key":"4_CR18","doi-asserted-by":"crossref","unstructured":"McKinna, J., Pollack, R.: James McKinna and Robert Pollack. Some lambda calculus and type theory formalized. Journal of Automated Reasoning\u00a023(3\u20134) (November 1999)","DOI":"10.1023\/A:1006294005493"},{"key":"4_CR19","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/2319.001.0001","volume-title":"The Definition of Standard ML, Revised edition","author":"R. Milner","year":"1997","unstructured":"Milner, R., Tofte, M., Harper, R., MacQueen, D.: The Definition of Standard ML, Revised edition. MIT Press, Cambridge (1997)"},{"key":"4_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1007\/978-3-540-40007-3_11","volume-title":"Formal Methods at the Crossroads. From Panacea to Foundational Support","author":"J.S. Moore","year":"2003","unstructured":"Moore, J.S.: A grand challenge proposal for formal methods: A verified stack. In: Aichernig, B.K., Maibaum, T. (eds.) Formal Methods at the Crossroads. From Panacea to Foundational Support. LNCS, vol.\u00a02757, pp. 161\u2013172. Springer, Heidelberg (2003)"},{"issue":"3","key":"4_CR21","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1145\/514188.514189","volume":"24","author":"J.S. Moore","year":"2002","unstructured":"Moore, J.S., Porter, G.: The apprentice challenge. ACM Trans. Program. Lang. Syst.\u00a024(3), 193\u2013216 (2002)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"4_CR22","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1023\/A:1006277616879","volume":"23","author":"W. Naraschewski","year":"1999","unstructured":"Naraschewski, W., Nipkow, T.: Type inference verified: Algorithm W in Isabelle\/HOL. Journal of Automated Reasoning\u00a023, 299\u2013318 (1999)","journal-title":"Journal of Automated Reasoning"},{"key":"4_CR23","first-page":"117","volume-title":"Foundations of Secure Computation. Proc. Int. Summer School Marktoberdorf 1999","author":"T. Nipkow","year":"2000","unstructured":"Nipkow, T., von Oheimb, D., Pusch, C.: \u03bcJava: Embedding a programming language in a theorem prover. In: Bauer, F.L., Steinbr\u00fcggen, R. (eds.) Foundations of Secure Computation. Proc. Int. Summer School Marktoberdorf 1999, pp. 117\u2013144. IOS Press, Amsterdam (2000)"},{"key":"4_CR24","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1145\/268946.268960","volume-title":"POPL 1998: Proceedings of the 25th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","author":"T. Nipkow","year":"1998","unstructured":"Nipkow, T., von Oheimb, D.: Javalight is type-safe\u2014definitely. In: POPL 1998: Proceedings of the 25th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 161\u2013170. ACM Press, New York (1998)"},{"key":"4_CR25","unstructured":"Norrish, M.: Formalising C in HOL. PhD thesis, Computer Laboratory, University of Cambridge (1998)"},{"key":"4_CR26","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/976571.976577","volume-title":"MERLIN 2003: Proceedings Of The 2003 Workshop On Mechanized Reasoning About Languages With Variable Binding","author":"M. Norrish","year":"2003","unstructured":"Norrish, M.: Mechanising Hankin and Barendregt using the Gordon-Melham axioms. In: MERLIN 2003: Proceedings Of The 2003 Workshop On Mechanized Reasoning About Languages With Variable Binding, pp. 1\u20137. ACM Press, New York (2003)"},{"key":"4_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1007\/978-3-540-30142-4_18","volume-title":"Theorem Proving in Higher Order Logics","author":"M. Norrish","year":"2004","unstructured":"Norrish, M.: Recursive function definition for types with binders. In: Slind, K., Bunker, A., Gopalakrishnan, G.C. (eds.) TPHOLs 2004. LNCS, vol.\u00a03223, pp. 241\u2013256. Springer, Heidelberg (2004)"},{"key":"4_CR28","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1145\/53990.54010","volume-title":"PLDI 1988: Proceedings of the ACM SIGPLAN 1988 Conference on Programming Language Design and Implementation","author":"F. Pfenning","year":"1988","unstructured":"Pfenning, F., Elliot, C.: Higher-order abstract syntax. In: PLDI 1988: Proceedings of the ACM SIGPLAN 1988 Conference on Programming Language Design and Implementation, pp. 199\u2013208. ACM Press, New York (1988)"},{"key":"4_CR29","volume-title":"Types and Programming Languages","author":"B.C. Pierce","year":"2002","unstructured":"Pierce, B.C.: Types and Programming Languages. MIT Press, Cambridge (2002)"},{"issue":"2","key":"4_CR30","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."},{"issue":"2","key":"4_CR31","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1023\/A:1005806324129","volume":"21","author":"G. Sutcliffe","year":"1998","unstructured":"Sutcliffe, G., Suttner, C.: The TPTP problem library. Journal of Automated Reasoning\u00a021(2), 177\u2013203 (1998)","journal-title":"Journal of Automated Reasoning"},{"key":"4_CR32","doi-asserted-by":"crossref","unstructured":"Syme, D.: Reasoning with the formal definition of Standard ML in HOL. In: Joyce and Seger [16], pp. 43\u201360","DOI":"10.1007\/3-540-57826-9_124"},{"key":"4_CR33","unstructured":"Urban, C., Tasson, C.: Nominal techniques in Isabelle\/HOL. Accepted at CADE-20 in Tallinn. See http:\/\/www.mathematik.uni-muenchen.de\/~urban\/nominal\/"},{"key":"4_CR34","doi-asserted-by":"crossref","unstructured":"VanInwegen, M., Gunter, E.: HOL-ML. In: Joyce and Seger [16], pp. 61\u201374","DOI":"10.1007\/3-540-57826-9_125"},{"key":"4_CR35","series-title":"Electronic Notes in Theoretical Computer Science","volume-title":"Mechanized Reasoning about Languages with Variable Binding (MERLIN)","author":"R. Vestergaard","year":"2001","unstructured":"Vestergaard, R., Brotherston, J.: The mechanisation of Barendregt-style equational proofs (the residual perspective). In: Mechanized Reasoning about Languages with Variable Binding (MERLIN). Electronic Notes in Theoretical Computer Science, vol.\u00a058. Elsevier, Amsterdam (2001)"},{"issue":"2","key":"4_CR36","doi-asserted-by":"publisher","first-page":"212","DOI":"10.1016\/S0890-5401(03)00023-3","volume":"183","author":"R. Vestergaard","year":"2003","unstructured":"Vestergaard, R., Brotherston, J.: A formalised first-order confluence proof for the \u03bb-calculus using one-sorted variable names. RTA 2001\u00a0183(2), 212\u2013244 (2003); Special edition with selected papers from RTA 2001","journal-title":"Information and Computation"}],"container-title":["Lecture Notes in Computer Science","Theorem Proving in Higher Order Logics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11541868_4.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T20:18:15Z","timestamp":1605644295000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11541868_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540283720","9783540318200"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/11541868_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2005]]}}}