{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,23]],"date-time":"2026-02-23T23:09:48Z","timestamp":1771888188047,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642396335","type":"print"},{"value":"9783642396342","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-39634-2_10","type":"book-chapter","created":{"date-parts":[[2013,7,22]],"date-time":"2013-07-22T09:52:36Z","timestamp":1374486756000},"page":"100-115","source":"Crossref","is-referenced-by-count":43,"title":["Data Refinement in Isabelle\/HOL"],"prefix":"10.1007","author":[{"given":"Florian","family":"Haftmann","sequence":"first","affiliation":[]},{"given":"Alexander","family":"Krauss","sequence":"additional","affiliation":[]},{"given":"Ond\u0159ej","family":"Kun\u010dar","sequence":"additional","affiliation":[]},{"given":"Tobias","family":"Nipkow","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"10_CR1","doi-asserted-by":"crossref","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development. Springer (2004)","DOI":"10.1007\/978-3-662-07964-5"},{"key":"10_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"12","DOI":"10.1007\/978-3-642-24364-6_2","volume-title":"Frontiers of Combining Systems","author":"J.C. Blanchette","year":"2011","unstructured":"Blanchette, J.C., Bulwahn, L., Nipkow, T.: Automatic Proof and Disproof in Isabelle\/HOL. In: Tinelli, C., Sofronie-Stokkermans, V. (eds.) FroCoS 2011. LNCS, vol.\u00a06989, pp. 12\u201327. Springer, Heidelberg (2011)"},{"key":"10_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"370","DOI":"10.1007\/978-3-540-24725-8_26","volume-title":"Programming Languages and Systems","author":"J.-C. Filli\u00e2tre","year":"2004","unstructured":"Filli\u00e2tre, J.-C., Letouzey, P.: Functors for Proofs and Programs. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol.\u00a02986, pp. 370\u2013384. Springer, Heidelberg (2004)"},{"key":"10_CR4","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1017\/S0956796807006338","volume":"18","author":"D. Greve","year":"2008","unstructured":"Greve, D., Kaufmann, M., Manolios, P., Moore, J., Ray, S., Ruiz-Reina, J., Sumners, R., Vroon, D., Wilding, M.: Efficient execution in an automated reasoning environment. J. Functional Programming\u00a018, 15\u201346 (2008)","journal-title":"J. Functional Programming"},{"key":"10_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1007\/978-3-642-12251-4_9","volume-title":"Functional and Logic Programming","author":"F. Haftmann","year":"2010","unstructured":"Haftmann, F., Nipkow, T.: Code Generation via Higher-Order Rewrite Systems. In: Blume, M., Kobayashi, N., Vidal, G. (eds.) FLOPS 2010. LNCS, vol.\u00a06009, pp. 103\u2013117. Springer, Heidelberg (2010)"},{"key":"10_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/3-540-16442-1_14","volume-title":"ESOP 86","author":"J. He","year":"1986","unstructured":"He, J., Hoare, C.A.R., Sanders, J.W.: Data refinement refined. In: Robinet, B., Wilhelm, R. (eds.) ESOP 1986. LNCS, vol.\u00a0213, pp. 187\u2013196. Springer, Heidelberg (1986)"},{"key":"10_CR7","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1007\/BF00289507","volume":"1","author":"C.A.R. Hoare","year":"1972","unstructured":"Hoare, C.A.R.: Proof of Correctness of Data Representations. Acta Informatica\u00a01, 271\u2013281 (1972)","journal-title":"Acta Informatica"},{"key":"10_CR8","doi-asserted-by":"crossref","unstructured":"Huffman, B., Kun\u010dar, O.: Lifting and Transfer: A Modular Design for Quotients in Isabelle\/HOL. Presented at the Isabelle Users Workshop at ITP 2012 (2012), \n                    \n                      http:\/\/www21.in.tum.de\/~kuncar\/huffman-kuncar-itp2012.pdf","DOI":"10.1007\/978-3-319-03545-1_9"},{"key":"10_CR9","unstructured":"Jones, C.B.: Software Development. A Rigourous Approach. Prentice Hall (1980)"},{"key":"10_CR10","doi-asserted-by":"crossref","unstructured":"Kaliszyk, C., Urban, C.: Quotients revisited for Isabelle\/HOL. In: Chu, W.C., Wong, W.E., Palakal, M.J., Hung, C.-C. (eds.) Proc. of the 26th ACM Symposium on Applied Computing (SAC 2011), pp. 1639\u20131644. ACM (2011)","DOI":"10.1145\/1982185.1982529"},{"key":"10_CR11","doi-asserted-by":"crossref","unstructured":"Kaufmann, M., Manolios, P., More, J.S.: Computer-Aided Reasoning: ACL2 Case Studies. Kluwer Academic Publishers (2000)","DOI":"10.1007\/978-1-4757-3188-0"},{"key":"10_CR12","series-title":"LNCS","first-page":"84","volume-title":"ITP 2013","author":"P. Lammich","year":"2013","unstructured":"Lammich, P.: Automatic data refinement. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol.\u00a07998, pp. 84\u201399. Springer, Heidelberg (2013)"},{"key":"10_CR13","series-title":"LNCS","first-page":"116","volume-title":"ITP 2013","author":"A. Lochbihler","year":"2013","unstructured":"Lochbihler, A.: Light-weight containers for Isabelle: efficient, extensible and nestable. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol.\u00a07998, pp. 116\u2013132. Springer, Heidelberg (2013)"},{"key":"10_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"216","DOI":"10.1007\/978-3-642-22863-6_17","volume-title":"Interactive Theorem Proving","author":"A. Lochbihler","year":"2011","unstructured":"Lochbihler, A., Bulwahn, L.: Animating the Formalised Semantics of a Java-like Language. In: van Eekelen, M., Geuvers, H., Schmaltz, J., Wiedijk, F. (eds.) ITP 2011. LNCS, vol.\u00a06898, pp. 216\u2013232. Springer, Heidelberg (2011)"},{"key":"10_CR15","doi-asserted-by":"publisher","first-page":"629","DOI":"10.1007\/BF00263649","volume":"22","author":"T. Nipkow","year":"1986","unstructured":"Nipkow, T.: Non-Deterministic Data Types: Models and Implementations. Acta Informatica\u00a022, 629\u2013661 (1986)","journal-title":"Acta Informatica"},{"key":"10_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"260","DOI":"10.1007\/BFb0039611","volume-title":"STACS 87","author":"T. Nipkow","year":"1987","unstructured":"Nipkow, T.: Are Homomorphisms Sufficient for Behavioural Implementations of Deterministic and Nondeterministic Data Types? In: Brandenburg, F.J., Vidal-Naquet, G., Wirsing, M. (eds.) STACS 1987. LNCS, vol.\u00a0247, pp. 260\u2013271. Springer, Heidelberg (1987)"},{"key":"10_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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":"10_CR18","unstructured":"Reif, W., Schellhorn, G., Stenzel, K.: Interactive Correctness Proofs for Software Modules Using KIV. In: COMPASS 1995: Proc. Tenth Annual Conf. Computer Assurance, pp. 151\u2013162. IEEE (1995)"},{"key":"10_CR19","unstructured":"Traytel, D., Nipkow, T.: A Verified Decision Procedure for MSO on Words (2013), \n                    \n                      http:\/\/www.in.tum.de\/~nipkow\/pubs"}],"container-title":["Lecture Notes in Computer Science","Interactive Theorem Proving"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-39634-2_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,15]],"date-time":"2019-05-15T22:36:23Z","timestamp":1557959783000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-39634-2_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642396335","9783642396342"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-39634-2_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013]]}}}