{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T02:46:06Z","timestamp":1767926766512,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642396335","type":"print"},{"value":"9783642396342","type":"electronic"}],"license":[{"start":{"date-parts":[[2013,1,1]],"date-time":"2013-01-01T00:00:00Z","timestamp":1356998400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-39634-2_9","type":"book-chapter","created":{"date-parts":[[2013,7,22]],"date-time":"2013-07-22T13:52:36Z","timestamp":1374501156000},"page":"84-99","source":"Crossref","is-referenced-by-count":49,"title":["Automatic Data Refinement"],"prefix":"10.1007","author":[{"given":"Peter","family":"Lammich","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"9_CR1","unstructured":"Back, R.J.: On the correctness of refinement steps in program development. Ph.D. thesis, Department of Computer Science, University of Helsinki (1978)"},{"key":"9_CR2","doi-asserted-by":"crossref","unstructured":"Back, R.J., von Wright, J.: Refinement Calculus \u2014 A Systematic Introduction. Springer (1998)","DOI":"10.1007\/978-1-4612-1674-2"},{"key":"9_CR3","unstructured":"Backhouse, R.C., de Bruin, P., Malcolm, G., Voermans, E., van der Woude, J.: Relational catamorphisms. In: Proc. of the IFIP TC2\/WG2.1 Working Conference on Constructing Programs. Elsevier Science Publishers BV (1991)"},{"key":"9_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"92","DOI":"10.1007\/978-3-642-35308-6_10","volume-title":"Certified Programs and Proofs","author":"L. Bulwahn","year":"2012","unstructured":"Bulwahn, L.: The new quickcheck in Isabelle: Random, exhaustive and symbolic testing under one roof. In: Hawblitzel, C., Miller, D. (eds.) CPP 2012. LNCS, vol.\u00a07679, pp. 92\u2013108. Springer, Heidelberg (2012)"},{"key":"9_CR5","unstructured":"Eberl, M.: Efficient and Verified Computation of Simulation Relations on NFAs. Bachelor\u2019s thesis, Technische Universit\u00e4t M\u00fcnchen (2012)"},{"key":"9_CR6","doi-asserted-by":"crossref","unstructured":"Esparza, J., Lammich, P., Neumann, R., Nipkow, T., Schimpf, A., Smaus, J.G.: A fully verified executable LTL model checker. To appear in Proc. of CAV (2013)","DOI":"10.1007\/978-3-642-39799-8_31"},{"key":"9_CR7","unstructured":"Haftmann, F.: Code Generation from Specifications in Higher Order Logic. Ph.D. thesis, Technische Universit\u00e4t M\u00fcnchen (2009)"},{"key":"9_CR8","series-title":"LNCS","first-page":"100","volume-title":"ITP 2013","author":"F. Haftmann","year":"2013","unstructured":"Haftmann, F., Krauss, A., Kun\u010dar, O., Nipkow, T.: Data refinement in Isabelle\/HOL. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol.\u00a07998, pp. 100\u2013115. Springer, Heidelberg (2013)"},{"key":"9_CR9","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":"9_CR10","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":"9_CR11","doi-asserted-by":"crossref","unstructured":"Holzmann, G., Peled, D., Yannakakis, M.: On nested depth first search. In: Proc. of SPIN Workshop. Discrete Mathematics and Theoretical Computer Science, vol.\u00a032, pp. 23\u201332. American Mathematical Society (1997)","DOI":"10.1090\/dimacs\/032\/03"},{"key":"9_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1007\/978-3-642-03359-9_18","volume-title":"Theorem Proving in Higher Order Logics","author":"P.V. Homeier","year":"2009","unstructured":"Homeier, P.V.: The HOL-Omega logic. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol.\u00a05674, pp. 244\u2013259. Springer, Heidelberg (2009)"},{"key":"9_CR13","doi-asserted-by":"crossref","unstructured":"Huffman, B., Kun\u010dar, O.: Lifting and transfer: A modular design for quotients in Isabelle\/HOL. In: Isabelle Users Workshop 2012 (2012)","DOI":"10.1007\/978-3-319-03545-1_9"},{"key":"9_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"112","DOI":"10.1007\/978-3-540-27812-2_11","volume-title":"Theory Is Forever","author":"L. Ilie","year":"2004","unstructured":"Ilie, L., Navarro, G., Yu, S.: On NFA reductions. In: Karhum\u00e4ki, J., Maurer, H., P\u0103un, G., Rozenberg, G. (eds.) Theory Is Forever. LNCS, vol.\u00a03113, pp. 112\u2013124. Springer, Heidelberg (2004)"},{"key":"9_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"339","DOI":"10.1007\/978-3-642-14052-5_24","volume-title":"Interactive Theorem Proving","author":"P. Lammich","year":"2010","unstructured":"Lammich, P., Lochbihler, A.: The Isabelle Collections Framework. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol.\u00a06172, pp. 339\u2013354. Springer, Heidelberg (2010)"},{"key":"9_CR16","unstructured":"Lammich, P.: Collections framework. In: Archive of Formal Proofs, formal proof development (December 2009), \n                    \n                      http:\/\/afp.sf.net\/entries\/Collections.shtml"},{"key":"9_CR17","unstructured":"Lammich, P.: Tree automata. In: Archive of Formal Proofs, formal proof development (December 2009), \n                    \n                      http:\/\/afp.sf.net\/entries\/Tree-Automata.shtml"},{"key":"9_CR18","unstructured":"Lammich, P.: Refinement for monadic programs. In: Archive of Formal Proofs, formal proof development (2012), \n                    \n                      http:\/\/afp.sf.net\/entries\/Refine_Monadic.shtml"},{"key":"9_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"166","DOI":"10.1007\/978-3-642-32347-8_12","volume-title":"Interactive Theorem Proving","author":"P. Lammich","year":"2012","unstructured":"Lammich, P., Tuerk, T.: Applying data refinement for monadic programs to Hopcroft\u2019s algorithm. In: Beringer, L., Felty, A. (eds.) ITP 2012. LNCS, vol.\u00a07406, pp. 166\u2013182. Springer, Heidelberg (2012)"},{"key":"9_CR20","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":"9_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"13","DOI":"10.1007\/3-540-51084-2_2","volume-title":"Symbolic and Algebraic Computation","author":"D.R. Musser","year":"1989","unstructured":"Musser, D.R., Stepanov, A.A.: Generic programming. In: Gianni, P. (ed.) ISSAC 1988. LNCS, vol.\u00a0358, pp. 13\u201325. Springer, Heidelberg (1989)"},{"key":"9_CR22","doi-asserted-by":"crossref","unstructured":"Myreen, M.O., Owens, S.: Proof-producing synthesis of ML from higher-order logic. In: Proceedings of the 17th ACM SIGPLAN International Conference on Functional Programming, ICFP 2012, pp. 115\u2013126. ACM (2012)","DOI":"10.1145\/2364527.2364545"},{"key":"9_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL \u2014 A Proof Assistant for Higher-Order Logic","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.T.: Isabelle\/HOL. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"key":"9_CR24","unstructured":"Nordhoff, B., Lammich, P.: Formalization of Dijkstra\u2019s algorithm, formal proof development (2012)"},{"key":"9_CR25","unstructured":"Reynolds, J.C.: Types, abstraction and parametric polymorphism. In: IFIP Congress, pp. 513\u2013523 (1983)"},{"key":"9_CR26","doi-asserted-by":"crossref","unstructured":"Wadler, P.: Theorems for free! In: Proc. of FPCA, pp. 347\u2013359. ACM (1989)","DOI":"10.1145\/99370.99404"}],"container-title":["Lecture Notes in Computer Science","Interactive Theorem Proving"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-39634-2_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,20]],"date-time":"2019-05-20T01:51:24Z","timestamp":1558317084000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-39634-2_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642396335","9783642396342"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-39634-2_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013]]}}}