{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,11,11]],"date-time":"2026-11-11T12:52:51Z","timestamp":1794401571303,"version":"4.9.0"},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642246890","type":"print"},{"value":"9783642246906","type":"electronic"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"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":[[2011]]},"DOI":"10.1007\/978-3-642-24690-6_24","type":"book-chapter","created":{"date-parts":[[2011,10,24]],"date-time":"2011-10-24T21:35:37Z","timestamp":1319492137000},"page":"350-365","source":"Crossref","is-referenced-by-count":22,"title":["Using Coq in Specification and Program Extraction of Hadoop MapReduce Applications"],"prefix":"10.1007","author":[{"given":"Kosuke","family":"Ono","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Yoichi","family":"Hirai","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Yoshinori","family":"Tanabe","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Natsuko","family":"Noda","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Masami","family":"Hagiya","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"24_CR1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-07964-5","volume-title":"Interactive Theorem Proving and Program Development","author":"Y. Bertot","year":"2004","unstructured":"Bertot, Y., Casteran, P.: Interactive Theorem Proving and Program Development. Springer, Heidelberg (2004)"},{"key":"24_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"342","DOI":"10.1007\/11804192_16","volume-title":"Formal Methods for Components and Objects","author":"P. Chalin","year":"2006","unstructured":"Chalin, P., Kiniry, J., Leavens, G., Poll, E.: Beyond assertions: Advanced specification and verification with JML and ESC\/Java2. In: de Boer, F., Bonsangue, M., Graf, S., de Roever, W.P. (eds.) FMCO 2005. LNCS, vol.\u00a04111, pp. 342\u2013363. Springer, Heidelberg (2006)"},{"key":"24_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"270","DOI":"10.1007\/10930755_18","volume-title":"Theorem Proving in Higher Order Logics","author":"J. Chrz\u0105szcz","year":"2003","unstructured":"Chrz\u0105szcz, J.: Implementing modules in the Coq system. In: Basin, D., Wolff, B. (eds.) TPHOLs 2003. LNCS, vol.\u00a02758, pp. 270\u2013286. Springer, Heidelberg (2003)"},{"key":"24_CR4","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1145\/1327452.1327492","volume":"51","author":"J. Dean","year":"2008","unstructured":"Dean, J., Ghemawat, S.: Mapreduce: simplified data processing on large clusters. Commun. ACM\u00a051, 107\u2013113 (2008)","journal-title":"Commun. ACM"},{"key":"24_CR5","doi-asserted-by":"publisher","first-page":"365","DOI":"10.1145\/1066100.1066102","volume":"52","author":"D. Detlefs","year":"2005","unstructured":"Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: a theorem prover for program checking. J. ACM\u00a052, 365\u2013473 (2005)","journal-title":"J. ACM"},{"key":"24_CR6","volume-title":"MapReduce 2011","author":"J. D\u00f6rre","year":"2011","unstructured":"D\u00f6rre, J., Apel, S., Lengauer, C.: Static type checking of Hadoop MapReduce. In: MapReduce 2011. ACM, New York (to appear, 2011)"},{"key":"24_CR7","unstructured":"H\u00fcbel, T.: The Holumbus Framework. Master\u2019s thesis, Wedel University of Applied Sciences (2008)"},{"key":"24_CR8","doi-asserted-by":"crossref","unstructured":"Jimmy Lin, C.D.: Data-Intensive Text Processing with MapReduce. Morgan and Claypool (2010)","DOI":"10.2200\/S00274ED1V01Y201006HLT007"},{"issue":"1","key":"24_CR9","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.scico.2007.07.001","volume":"70","author":"R. L\u00e4mmel","year":"2008","unstructured":"L\u00e4mmel, R.: Google\u2019s MapReduce programming model \u2013 revisited. Science of Computer Programming\u00a070(1), 1\u201330 (2008)","journal-title":"Science of Computer Programming"},{"key":"24_CR10","unstructured":"Leavens, G.T., Poll, E., Clifton, C., Cheon, Y., Ruby, C., Cok, D., Muller, P., Kiniry, J., Chalin, P., Zimmerman, D.M.: JML reference manual (2011), http:\/\/www.eecs.ucf.edu\/~leavens\/JML\/documentation.shtml"},{"issue":"1-2","key":"24_CR11","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1016\/j.jlap.2003.07.006","volume":"58","author":"C. March\u00e9","year":"2004","unstructured":"March\u00e9, C., Paulin-Mohring, C., Urbain, X.: The KRAKATOA tool for certificationof JAVA\/JAVACARD programs annotated in JML. Journal of Logic and Algebraic Programming\u00a058(1-2), 89\u2013106 (2004)","journal-title":"Journal of Logic and Algebraic Programming"},{"key":"24_CR12","unstructured":"Marlow, S.: Haskell 2010 language report (2010), http:\/\/www.haskell.org\/onlinereport\/haskell2010\/"},{"key":"24_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L. Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8ner, N.: Z3: An efficient SMT solver. In: Ramakrishnan, C., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"24_CR14","volume-title":"Hadoop: The Definitive Guide","author":"T. White","year":"2009","unstructured":"White, T.: Hadoop: The Definitive Guide. O\u2019Reilly Media, Inc., Sebastopol (2009)"},{"key":"24_CR15","first-page":"358","volume-title":"Proceedings of the 2010 17th IEEE International Conference and Workshops on the Engineering of Computer-Based Systems, ECBS 2010","author":"F. Yang","year":"2010","unstructured":"Yang, F., Su, W., Zhu, H., Li, Q.: Formalizing MapReduce with CSP. In: Proceedings of the 2010 17th IEEE International Conference and Workshops on the Engineering of Computer-Based Systems, ECBS 2010, pp. 358\u2013367. IEEE, Los Alamitos (2010)"}],"container-title":["Lecture Notes in Computer Science","Software Engineering and Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-24690-6_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,18]],"date-time":"2019-06-18T10:33:59Z","timestamp":1560854039000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-24690-6_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642246890","9783642246906"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-24690-6_24","relation":{"is-part-of":[{"id-type":"doi","id":"https:\/\/doi.org\/10.1007\/978-3-642-24690-6","asserted-by":"object"}]},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011]]}}}