{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T06:08:35Z","timestamp":1725516515645},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540691471"},{"type":"electronic","value":"9783540691495"}],"license":[{"start":{"date-parts":[[2008,1,1]],"date-time":"2008-01-01T00:00:00Z","timestamp":1199145600000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2008]]},"DOI":"10.1007\/978-3-540-69149-5_3","type":"book-chapter","created":{"date-parts":[[2008,8,12]],"date-time":"2008-08-12T12:07:43Z","timestamp":1218542863000},"page":"26-30","source":"Crossref","is-referenced-by-count":3,"title":["It Is Time to Mechanize Programming Language Metatheory"],"prefix":"10.1007","author":[{"given":"Benjamin C.","family":"Pierce","sequence":"first","affiliation":[]},{"given":"Peter","family":"Sewell","sequence":"additional","affiliation":[]},{"given":"Stephanie","family":"Weirich","sequence":"additional","affiliation":[]},{"given":"Steve","family":"Zdancewic","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"3_CR1","doi-asserted-by":"crossref","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: Theorem Proving in Higher Order Logics, 18th International Conference, Oxford, UK (August 2005)","DOI":"10.1007\/11541868_4"},{"key":"3_CR2","volume-title":"EATCS Texts in Theoretical Computer Science","author":"Y. Bertot","year":"2004","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development. In: EATCS Texts in Theoretical Computer Science, vol.\u00a0XXV, Springer, Heidelberg (2004)"},{"key":"3_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"750","DOI":"10.1007\/3-540-54415-1_73","volume-title":"Theoretical Aspects of Computer Software","author":"L. Cardelli","year":"1991","unstructured":"Cardelli, L., Martini, S., Mitchell, J.C., Scedrov, A.: An extension of System F with subtyping. In: Ito, T., Meyer, A.R. (eds.) TACS 1991. LNCS, vol.\u00a0526, pp. 750\u2013770. Springer, Heidelberg (1991)"},{"issue":"4","key":"3_CR4","doi-asserted-by":"publisher","first-page":"471","DOI":"10.1145\/6041.6042","volume":"17","author":"L. Cardelli","year":"1985","unstructured":"Cardelli, L., Wegner, P.: On understanding types, data abstraction, and polymorphism. Computing Surveys\u00a017(4), 471\u2013522 (1985)","journal-title":"Computing Surveys"},{"key":"3_CR5","volume-title":"Implementing Mathematics with the NuPRL Proof Development System","author":"R.L. Constable","year":"1986","unstructured":"Constable, R.L., Allen, S.F., Bromley, M., Cleaveland, R., Cremer, J.F., Harper, R.W., Howe, D.J., Knoblock, T.B., Mendler, P., Panangaden, P., Sasaki, J.T., Smith, S.F.: Implementing Mathematics with the NuPRL Proof Development System. Prentice-Hall, Englewood Cliffs, NJ (1986)"},{"key":"3_CR6","first-page":"55","volume-title":"Theoretical Aspects of Object-Oriented Programming: Types, Semantics, and Language Design","author":"P.-L. Curien","year":"1994","unstructured":"Curien, P.-L., Ghelli, G.: Coherence of subsumption: Minimum typing and type-checking in F. Mathematical Structures in Computer Science. In: Gunter, C.A., Mitchell, J.C. (eds.) Theoretical Aspects of Object-Oriented Programming: Types, Semantics, and Language Design, vol.\u00a02, pp. 55\u201391. MIT Press, Cambridge (1994)"},{"key":"3_CR7","unstructured":"Dennis, L.A.: Inductive challenge problems (2000), http:\/\/www.cs.nott.ac.uk\/~lad\/research\/challenges"},{"key":"3_CR8","series-title":"Proceedings of Symposia in Applied Mathematics","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1090\/psapm\/019\/0235771","volume-title":"Mathematical Aspects of Computer Science","author":"R.W. Floyd","year":"1967","unstructured":"Floyd, R.W.: Assigning meanings to programs. In: Schwartz, J.T. (ed.) Mathematical Aspects of Computer Science. Proceedings of Symposia in Applied Mathematics, vol.\u00a019, pp. 19\u201332. American Mathematical Society, Providence, Rhode Island (1967)"},{"key":"3_CR9","doi-asserted-by":"crossref","unstructured":"Gent, I.P., Walsh, T.: CSPLib: a benchmark library for constraints. Technical report, Technical report APES-09-, 1999. A shorter version appears in the Proceedings of the 5th International Conference on Principles and Practices of Constraint Programming (CP-99) (1999), http:\/\/csplib.cs.strath.ac.uk\/","DOI":"10.1007\/978-3-540-48085-3_36"},{"volume-title":"Introduction to HOL: a theorem proving environment for higher order logic","year":"1993","key":"3_CR10","unstructured":"Gordon, M.J.C., Melham, T.F. (eds.): Introduction to HOL: a theorem proving environment for higher order logic. Cambridge University Press, Cambridge (1993)"},{"key":"3_CR11","unstructured":"Green, I.: The dream corpus of inductive conjectures (1999), http:\/\/dream.dai.ed.ac.uk\/dc\/lib.html"},{"issue":"1","key":"3_CR12","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":"3_CR13","unstructured":"Hoos, H., Stuetzle, T.: Satlib, http:\/\/www.intellektik.informatik.tu-darmstadt.de\/SATLIB\/"},{"key":"3_CR14","doi-asserted-by":"crossref","unstructured":"Igarashi, A., Pierce, B., Wadler, P.: Featherweight Java: A minimal core calculus for Java and GJ. In: ACM SIGPLAN Conference on Object Oriented Programming: Systems, Languages, and Applications (OOPSLA) October 1999. Full version in ACM Transactions on Programming Languages and Systems (TOPLAS), vol. 23(3) ( May 2001)","DOI":"10.1145\/503502.503505"},{"key":"3_CR15","volume-title":"Computer-Aided Reasoning: An Approach","author":"M. Kaufmann","year":"2000","unstructured":"Kaufmann, M., Moore, J.S., Manolios, P.: Computer-Aided Reasoning: An Approach. Kluwer Academic Publishers, Dordrecht (2000)"},{"key":"3_CR16","unstructured":"Luo, Z., Pollack, R.: The LEGO proof development system: A user\u2019s manual. Technical Report ECS-LFCS-92-211, University of Edinburgh (May 1992)"},{"key":"3_CR17","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":"3_CR18","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.S.E. (eds.) Formal Methods at the Crossroads. From Panacea to Foundational Support. LNCS, vol.\u00a02757, pp. 161\u2013172. Springer, Heidelberg (2003)"},{"issue":"3","key":"3_CR19","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":"3_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.T.: Isabelle\/HOL. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"key":"3_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"411","DOI":"10.1007\/3-540-61474-5_91","volume-title":"Computer Aided Verification","author":"S. Owre","year":"1996","unstructured":"Owre, S., Rajan, S., Rushby, J.M., Shankar, N., Srivas, M.K.: PVS: Combining specification, proof checking, and model checking. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol.\u00a01102, pp. 411\u2013414. Springer, Heidelberg (1996)"},{"key":"3_CR22","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 \u2014 A meta-logical framework for deductive systems. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol.\u00a01632, pp. 202\u2013206. Springer, Heidelberg (1999)"},{"issue":"2","key":"3_CR23","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"}],"container-title":["Lecture Notes in Computer Science","Verified Software: Theories, Tools, Experiments"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-69149-5_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,13]],"date-time":"2019-05-13T03:42:56Z","timestamp":1557718976000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-69149-5_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008]]},"ISBN":["9783540691471","9783540691495"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-69149-5_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2008]]}}}