{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,16]],"date-time":"2026-10-16T20:24:18Z","timestamp":1792182258287,"version":"4.4.0"},"publisher-location":"Berlin, Heidelberg","reference-count":54,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540710653","type":"print"},{"value":"9783540710677","type":"electronic"}],"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-71067-7_7","type":"book-chapter","created":{"date-parts":[[2008,10,3]],"date-time":"2008-10-03T08:55:16Z","timestamp":1223024116000},"page":"33-38","source":"Crossref","is-referenced-by-count":108,"title":["The Isabelle Framework"],"prefix":"10.1007","author":[{"given":"Makarius","family":"Wenzel","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Lawrence C.","family":"Paulson","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Tobias","family":"Nipkow","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"7_CR1","series-title":"Lecture Notes in Computer Science","volume-title":"Theorem Proving in Higher Order Logics (TPHOLs 2008)","author":"K. Aehlig","year":"2008","unstructured":"Aehlig, K., Haftmann, F., Nipkow, T.: A compiled implementation of normalization by evaluation. In: Theorem Proving in Higher Order Logics (TPHOLs 2008). LNCS. Springer, Heidelberg (2008)"},{"key":"7_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1007\/978-3-540-78800-3_9","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2008)","author":"E. Alkassar","year":"2008","unstructured":"Alkassar, E., Schirmer, N., Starostin, A.: Formal pervasive verification of a paging mechanism. In: Ramakrishnan, C.R., Rehof, J. (eds.) Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2008). LNCS, vol.\u00a04963, pp. 109\u2013123. Springer, Heidelberg (2008)"},{"key":"7_CR3","doi-asserted-by":"crossref","unstructured":"Aspinall, D.: Proof General: A generic tool for proof development. In: European Joint Conferences on Theory and Practice of Software (ETAPS) (2000)","DOI":"10.1007\/3-540-46419-0_3"},{"issue":"1:2","key":"7_CR4","first-page":"1","volume":"9","author":"J. Avigad","year":"2007","unstructured":"Avigad, J., Donnelly, K., Gray, D., Raff, P.: A formally verified proof of the prime number theorem. ACM Trans. Comput. Logic\u00a09(1:2), 1\u201323 (2007)","journal-title":"ACM Trans. Comput. Logic"},{"key":"7_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24849-1_3","volume-title":"Types for Proofs and Programs","author":"C. Ballarin","year":"2004","unstructured":"Ballarin, C.: Locales and locale expressions in Isabelle\/Isar. In: Berardi, S., Coppo, M., Damiani, F. (eds.) TYPES 2003. LNCS, vol.\u00a03085. Springer, Heidelberg (2004)"},{"key":"7_CR6","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","DOI":"10.1007\/11812289_4","volume-title":"Mathematical Knowledge Management","author":"C. Ballarin","year":"2006","unstructured":"Ballarin, C.: Interpretation of locales in Isabelle: Theories and proof contexts. In: Borwein, J.M., Farmer, W.M. (eds.) MKM 2006. LNCS (LNAI), vol.\u00a04108. Springer, Heidelberg (2006)"},{"key":"7_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44755-5_7","volume-title":"Theorem Proving in Higher Order Logics","author":"G. Bauer","year":"2001","unstructured":"Bauer, G., Wenzel, M.: Calculational reasoning revisited \u2014 an Isabelle\/Isar experience. In: Boulton, R.J., Jackson, P.B. (eds.) TPHOLs 2001. LNCS, vol.\u00a02152. Springer, Heidelberg (2001)"},{"key":"7_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44659-1_3","volume-title":"Theorem Proving in Higher Order Logics","author":"S. Berghofer","year":"2000","unstructured":"Berghofer, S., Nipkow, T.: Proof terms for simply typed higher order logic. In: Aagaard, M.D., Harrison, J. (eds.) TPHOLs 2000. LNCS, vol.\u00a01869. Springer, Heidelberg (2000)"},{"key":"7_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1007\/3-540-45842-5_2","volume-title":"Types for Proofs and Programs","author":"S. Berghofer","year":"2002","unstructured":"Berghofer, S., Nipkow, T.: Executing higher order logic. In: Callaghan, P., Luo, Z., McKinna, J., Pollack, R. (eds.) TYPES 2000. LNCS, vol.\u00a02277, pp. 24\u201340. Springer, Heidelberg (2002)"},{"key":"7_CR10","first-page":"230","volume-title":"Software Engineering and Formal Methods (SEFM 2004)","author":"S. Berghofer","year":"2004","unstructured":"Berghofer, S., Nipkow, T.: Random testing in Isabelle\/HOL. In: Cuellar, J., Liu, Z. (eds.) Software Engineering and Formal Methods (SEFM 2004), pp. 230\u2013239. IEEE Computer Society Press, Los Alamitos (2004)"},{"key":"7_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48256-3_3","volume-title":"Theorem Proving in Higher Order Logics","author":"S. Berghofer","year":"1999","unstructured":"Berghofer, S., Wenzel, M.: Inductive datatypes in HOL \u2014 lessons learned in Formal-Logic Engineering. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Th\u00e9ry, L. (eds.) TPHOLs 1999. LNCS, vol.\u00a01690. Springer, Heidelberg (1999)"},{"key":"7_CR12","series-title":"Lecture Notes in Artificial Intelligence","volume-title":"Mathematical Knowledge Management (MKM 2008),","author":"S. Berghofer","year":"2008","unstructured":"Berghofer, S., Wenzel, M.: Logic-free reasoning in Isabelle\/Isar. In: Mathematical Knowledge Management (MKM 2008), LNCS (LNAI). Springer, Heidelberg (2008)"},{"key":"7_CR13","unstructured":"Bortin, M., Broch Johnsen, E., L\u00fcth, C.: Structured formal development in Isabelle. Nordic Journal of Computing 13 (2006)"},{"key":"7_CR14","series-title":"Lecture Notes in Computer Science","volume-title":"Theorem Proving in Higher Order Logics (TPHOLs 2008)","author":"L. Bulwahn","year":"2008","unstructured":"Bulwahn, L., Krauss, A., Haftmann, F., Erk\u00f6k, L., Matthews, J.: Imperative functional programming in Isabelle\/HOL. In: Theorem Proving in Higher Order Logics (TPHOLs 2008). LNCS. Springer, Heidelberg (2008)"},{"key":"7_CR15","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73086-6_3","volume-title":"Towards Mechanized Mathematical Assistants","author":"A. Chaieb","year":"2007","unstructured":"Chaieb, A., Wenzel, M.: Context aware calculation and deduction \u2014 ring equalities via Gr\u00f6bner Bases in Isabelle. In: Kauers, M., et al. (eds.) MKM\/CALCULEMUS 2007. LNCS (LNAI), vol.\u00a04573. Springer, Heidelberg (2007)"},{"key":"7_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-09724-4","volume-title":"Edinburgh LCF: A Mechanized Logic of Computation","author":"M.J.C. Gordon","year":"1979","unstructured":"Gordon, M.J.C., Milner, R., Wadsworth, C.P.: Edinburgh LCF. LNCS, vol.\u00a078. Springer, Heidelberg (1979)"},{"key":"7_CR17","unstructured":"Haftmann, F., Nipkow, T.: A code generator framework for Isabelle\/HOL. In: K.\u00a0Schneider, J.\u00a0Brandt (eds.) Theorem Proving in Higher Order Logics: Emerging Trends Proceedings. Dept. Comp. Sci., U. Kaiserslautern (2007)"},{"key":"7_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74464-1_11","volume-title":"Types for Proofs and Programs","author":"F. Haftmann","year":"2007","unstructured":"Haftmann, F., Wenzel, M.: Constructive type classes in Isabelle. In: Altenkirch, T., McBride, C. (eds.) TYPES 2006. LNCS, vol.\u00a04502. Springer, Heidelberg (2007)"},{"key":"7_CR19","doi-asserted-by":"crossref","unstructured":"Haftmann, F., Wenzel, M.: Local theory specifications in Isabelle\/Isar (2008), http:\/\/www.in.tum.de\/~wenzelm\/papers\/local-theory.pdf","DOI":"10.1007\/978-3-642-02444-3_10"},{"issue":"4","key":"7_CR20","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1145\/1278901.1278904","volume":"41","author":"G. Heiser","year":"2007","unstructured":"Heiser, G., Elphinstone, K., Kuz, I., Klein, G., Petters, S.M.: Towards trustworthy computing systems: taking microkernels to the next level. SIGOPS Operating Systems Review\u00a041(4), 3\u201311 (2007)","journal-title":"SIGOPS Operating Systems Review"},{"key":"7_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48256-3_11","volume-title":"Theorem Proving in Higher Order Logics","author":"F. Kamm\u00fcller","year":"1999","unstructured":"Kamm\u00fcller, F., Wenzel, M., Paulson, L.C.: Locales: A sectioning concept for Isabelle. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Th\u00e9ry, L. (eds.) TPHOLs 1999. LNCS, vol.\u00a01690. Springer, Heidelberg (1999)"},{"issue":"4","key":"7_CR22","doi-asserted-by":"publisher","first-page":"619","DOI":"10.1145\/1146809.1146811","volume":"28","author":"G. Klein","year":"2006","unstructured":"Klein, G., Nipkow, T.: A machine-checked model for a Java-like language, virtual machine and compiler. ACM Trans. Progr. Lang. Syst.\u00a028(4), 619\u2013695 (2006), http:\/\/doi.acm.org\/10.1145\/1146809.1146811","journal-title":"ACM Trans. Progr. Lang. Syst."},{"key":"7_CR23","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","DOI":"10.1007\/11814771_48","volume-title":"Automated Reasoning","author":"A. Krauss","year":"2006","unstructured":"Krauss, A.: Partial recursive functions in Higher-Order Logic. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol.\u00a04130. Springer, Heidelberg (2006)"},{"key":"7_CR24","volume-title":"Workshop on Systems Software Verification (SSV 2008)","author":"D. Leinenbach","year":"2008","unstructured":"Leinenbach, D., Petrova, E.: Pervasive compiler verification \u2014 from verified programs to verified systems. In: Workshop on Systems Software Verification (SSV 2008). Elsevier, Amsterdam (2008)"},{"key":"7_CR25","unstructured":"Lochbihler, A.: Type safe nondeterminism \u2014 a formal semantics of Java threads. In: Foundations of Object-Oriented Languages (FOOL 2008) (2008)"},{"key":"7_CR26","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1017\/S095679689900341X","volume":"9","author":"O. M\u00fcller","year":"1999","unstructured":"M\u00fcller, O., Nipkow, T., von Oheimb, D., Slotosch, O.: HOLCF = HOL + LCF. Journal of Functional Programming\u00a09, 191\u2013223 (1999)","journal-title":"Journal of Functional Programming"},{"key":"7_CR27","volume-title":"Logical Environments","author":"T. Nipkow","year":"1993","unstructured":"Nipkow, T.: Order-sorted polymorphism in Isabelle. In: Huet, G., Plotkin, G. (eds.) Logical Environments. Cambridge University Press, Cambridge (1993)"},{"key":"7_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-39185-1_15","volume-title":"Types for Proofs and Programs","author":"T. Nipkow","year":"2003","unstructured":"Nipkow, T.: Structured proofs in Isar\/HOL. In: Geuvers, H., Wiedijk, F. (eds.) TYPES 2002. LNCS, vol.\u00a02646. Springer, Heidelberg (2003)"},{"key":"7_CR29","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/11814771_4","volume-title":"Automated Reasoning","author":"T. Nipkow","year":"2006","unstructured":"Nipkow, T., Bauer, G., Schultz, P.: Flyspeck I: Tame graphs. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol.\u00a04130, pp. 21\u201335. Springer, Heidelberg (2006)"},{"key":"7_CR30","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.: Isabelle\/HOL. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"key":"7_CR31","unstructured":"Obua, S.: Flyspeck II: The basic linear programs. Ph.D. thesis, Technische Universit\u00e4t M\u00fcnchen (2008)"},{"key":"7_CR32","doi-asserted-by":"crossref","unstructured":"Paulson, L.C.: Natural deduction as higher-order resolution. Journal of Logic Programming 3 (1986)","DOI":"10.1016\/0743-1066(86)90015-4"},{"key":"7_CR33","volume-title":"Logic and Computer Science","author":"L.C. Paulson","year":"1990","unstructured":"Paulson, L.C.: Isabelle: the next 700 theorem provers. In: Odifreddi, P. (ed.) Logic and Computer Science. Academic Press, London (1990)"},{"key":"7_CR34","doi-asserted-by":"crossref","unstructured":"Paulson, L.C.: Set theory for verification: I. From foundations to functions. Journal of Automated Reasoning 11(3) (1993)","DOI":"10.1007\/BF00881873"},{"key":"7_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0030541","volume-title":"Automated Deduction - CADE-12","author":"L.C. Paulson","year":"1994","unstructured":"Paulson, L.C.: A fixedpoint approach to implementing (co)inductive definitions. In: Bundy, A. (ed.) CADE 1994. LNCS, vol.\u00a0814. Springer, Heidelberg (1994)"},{"key":"7_CR36","doi-asserted-by":"crossref","unstructured":"Paulson, L.C.: Set theory for verification: II. Induction and recursion. Journal of Automated Reasoning 15(2) (1995)","DOI":"10.1007\/BF00881916"},{"key":"7_CR37","volume-title":"Automated Reasoning and its Applications: Essays in Honor of Larry Wos","author":"L.C. Paulson","year":"1997","unstructured":"Paulson, L.C.: Generic automatic proof tools. In: Veroff, R. (ed.) Automated Reasoning and its Applications: Essays in Honor of Larry Wos. MIT Press, Cambridge (1997)"},{"key":"7_CR38","unstructured":"Paulson, L.C.: A generic tableau prover and its integration with Isabelle. Journal of Universal Computer Science 5(3) (1999)"},{"key":"7_CR39","doi-asserted-by":"crossref","unstructured":"Paulson, L.C.: The relative consistency of the axiom of choice \u2014 mechanized using Isabelle\/ZF. LMS Journal of Computation and Mathematics 6, 198\u2013248 (2003)","DOI":"10.1112\/S1461157000000449"},{"key":"7_CR40","doi-asserted-by":"crossref","unstructured":"Paulson, L.C.: Organizing numerical theories using axiomatic type classes. Journal of Automated Reasoning 33(1) (2004)","DOI":"10.1007\/s10817-004-3997-6"},{"key":"7_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74591-4_18","volume-title":"Theorem Proving in Higher Order Logics","author":"L.C. Paulson","year":"2007","unstructured":"Paulson, L.C., Susanto, K.W.: Source-level proof reconstruction for interactive theorem proving. In: Schneider, K., Brandt, J. (eds.) TPHOLs 2007. LNCS, vol.\u00a04732. Springer, Heidelberg (2007)"},{"key":"7_CR42","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0105417","volume-title":"Theorem Proving in Higher Order Logics","author":"K. Slind","year":"1996","unstructured":"Slind, K.: Function definition in higher order logic. In: von Wright, J., Harrison, J., Grundy, J. (eds.) TPHOLs 1996. LNCS, vol.\u00a01125. Springer, Heidelberg (1996)"},{"key":"7_CR43","first-page":"97","volume-title":"Principles of Programming Languages (POPL 2007)","author":"H. Tuch","year":"2007","unstructured":"Tuch, H., Klein, G., Norrish, M.: Types, bytes, and separation logic. In: Principles of Programming Languages (POPL 2007), pp. 97\u2013108. ACM Press, New York (2007)"},{"key":"7_CR44","doi-asserted-by":"publisher","first-page":"327","DOI":"10.1007\/s10817-008-9097-2","volume":"40","author":"C. Urban","year":"2008","unstructured":"Urban, C.: Nominal techniques in Isabelle\/HOL. Journal of Automated Reasoning\u00a040, 327\u2013356 (2008)","journal-title":"Journal of Automated Reasoning"},{"key":"7_CR45","doi-asserted-by":"crossref","unstructured":"Urban, C., Cheney, J., Berghofer, S.: Mechanizing the metatheory of LF. In: 23rd IEEE Symp. Logic in Computer Science (LICS) (2008)","DOI":"10.1109\/LICS.2008.29"},{"key":"7_CR46","first-page":"345","volume-title":"Object Oriented Programming, Systems, Languages, and Applications (OOPSLA 2006)","author":"D. Wasserrab","year":"2006","unstructured":"Wasserrab, D., Nipkow, T., Snelting, G., Tip, F.: An operational semantics and type safety proof for multiple inheritance in C++. In: Object Oriented Programming, Systems, Languages, and Applications (OOPSLA 2006), pp. 345\u2013362. ACM Press, New York (2006)"},{"key":"7_CR47","first-page":"103","volume-title":"Workshops Disproving and Pragmatics of Decision Procedures (PDPAR 2004)","author":"T. Weber","year":"2005","unstructured":"Weber, T.: Bounded model generation for Isabelle\/HOL. In: Ahrendt, W., Baumgartner, P., de Nivelle, H., Ranise, S., Tinelli, C. (eds.) Workshops Disproving and Pragmatics of Decision Procedures (PDPAR 2004), vol.\u00a0125, pp. 103\u2013116. Elsevier, Amsterdam (2005)"},{"key":"7_CR48","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0028402","volume-title":"Theorem Proving in Higher Order Logics","author":"M. Wenzel","year":"1997","unstructured":"Wenzel, M.: Type classes and overloading in higher-order logic. In: Gunter, E.L., Felty, A.P. (eds.) TPHOLs 1997. LNCS, vol.\u00a01275. Springer, Heidelberg (1997)"},{"key":"7_CR49","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48256-3_12","volume-title":"Theorem Proving in Higher Order Logics","author":"M. Wenzel","year":"1999","unstructured":"Wenzel, M.: Isar \u2014 a generic interpretative approach to readable formal proof documents. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Th\u00e9ry, L. (eds.) TPHOLs 1999. LNCS, vol.\u00a01690. Springer, Heidelberg (1999)"},{"key":"7_CR50","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","DOI":"10.1007\/11812289_3","volume-title":"Mathematical Knowledge Management","author":"M. Wenzel","year":"2006","unstructured":"Wenzel, M.: Structured induction proofs in Isabelle\/Isar. In: Borwein, J.M., Farmer, W.M. (eds.) MKM 2006. LNCS (LNAI), vol.\u00a04108. Springer, Heidelberg (2006)"},{"key":"7_CR51","unstructured":"Wenzel, M.: Isabelle\/Isar \u2014 a generic framework for human-readable proof documents. In: R.\u00a0Matuszewski, A.\u00a0Zalewska (eds.) From Insight to Proof \u2014 Festschrift in Honour of Andrzej Trybulec, Studies in Logic, Grammar, and Rhetoric, vol. 10(23). University of Bia\u0142ystok (2007), http:\/\/www.in.tum.de\/~wenzelm\/papers\/isar-framework.pdf"},{"key":"7_CR52","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","DOI":"10.1007\/11542384_8","volume-title":"The Seventeen Provers of the World","author":"M. Wenzel","year":"2006","unstructured":"Wenzel, M., Paulson, L.C.: Isabelle\/Isar. In: Wiedijk, F. (ed.) The Seventeen Provers of the World. LNCS (LNAI), vol.\u00a03600. Springer, Heidelberg (2006)"},{"key":"7_CR53","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74591-4_26","volume-title":"Theorem Proving in Higher Order Logics","author":"M. Wenzel","year":"2007","unstructured":"Wenzel, M., Wolff, B.: Building formal method tools in the Isabelle\/Isar framework. In: Schneider, K., Brandt, J. (eds.) TPHOLs 2007. LNCS, vol.\u00a04732. Springer, Heidelberg (2007)"},{"key":"7_CR54","doi-asserted-by":"crossref","unstructured":"Wiedijk, F., Wenzel, M.: A comparison of the mathematical proof languages Mizar and Isar. Journal of Automated Reasoning 29(3-4) (2002)","DOI":"10.1023\/A:1021935419355"}],"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\/978-3-540-71067-7_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,14]],"date-time":"2019-05-14T07:49:27Z","timestamp":1557820167000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-71067-7_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008]]},"ISBN":["9783540710653","9783540710677"],"references-count":54,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-71067-7_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2008]]}}}