{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T21:01:04Z","timestamp":1751662864044},"publisher-location":"Berlin, Heidelberg","reference-count":11,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642033582"},{"type":"electronic","value":"9783642033599"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"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":[[2009]]},"DOI":"10.1007\/978-3-642-03359-9_11","type":"book-chapter","created":{"date-parts":[[2009,8,20]],"date-time":"2009-08-20T01:46:12Z","timestamp":1250732772000},"page":"131-146","source":"Crossref","is-referenced-by-count":21,"title":["Turning Inductive into Equational Specifications"],"prefix":"10.1007","author":[{"given":"Stefan","family":"Berghofer","sequence":"first","affiliation":[]},{"given":"Lukas","family":"Bulwahn","sequence":"additional","affiliation":[]},{"given":"Florian","family":"Haftmann","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"11_CR1","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, p. 24. Springer, Heidelberg (2002)"},{"key":"11_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1007\/978-3-540-74591-4_7","volume-title":"Theorem Proving in Higher Order Logics","author":"D. Delahaye","year":"2007","unstructured":"Delahaye, D., Dubois, C., \u00c9tienne, J.F.: Extracting purely functional contents from logical inductive types. In: Schneider, K., Brandt, J. (eds.) TPHOLs 2007. LNCS, vol.\u00a04732, pp. 70\u201385. Springer, Heidelberg (2007)"},{"key":"11_CR3","unstructured":"Haftmann, F., Nipkow, T.: A code generator framework for Isabelle\/HOL. Tech. Rep. 364\/07, Department of Computer Science, University of Kaiserslautern (2007)"},{"key":"11_CR4","doi-asserted-by":"crossref","unstructured":"Hanus, M.: A unified computation model for functional and logic programming. In: Proc. 24th ACM Symposium on Principles of Programming Languages (POPL 1997), pp. 80\u201393 (1997)","DOI":"10.1145\/263699.263710"},{"key":"11_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"190","DOI":"10.1007\/978-3-540-72952-5_12","volume-title":"Formal Methods for Open Object-Based Distributed Systems","author":"L. Henrio","year":"2007","unstructured":"Henrio, L., Kamm\u00fcller, F.: A mechanized model of the theory of objects. In: Bonsangue, M.M., Johnsen, E.B. (eds.) FMOODS 2007. LNCS, vol.\u00a04468, pp. 190\u2013205. Springer, Heidelberg (2007)"},{"key":"11_CR6","unstructured":"Mellish, C.S.: The automatic generation of mode declarations for prolog programs. Tech. Rep. 163, Department of Artificial Intelligence (1981)"},{"key":"11_CR7","first-page":"117","volume-title":"Foundations of Secure Computation. Proc. Int. Summer School Marktoberdorf 1999","author":"T. Nipkow","year":"2000","unstructured":"Nipkow, T., von Oheimb, D., Pusch, C.: \u03bcJava: Embedding a programming language in a theorem prover. In: Bauer, F., Steinbr\u00fcggen, R. (eds.) Foundations of Secure Computation. Proc. Int. Summer School Marktoberdorf 1999, pp. 117\u2013144. IOS Press, Amsterdam (2000)"},{"key":"11_CR8","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.: Isabelle\/HOL. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"key":"11_CR9","unstructured":"Slind, K.: Reasoning about terminating functional programs. Ph.D. thesis, Institut f\u00fcr Informatik, TU M\u00fcnchen (1999)"},{"key":"11_CR10","unstructured":"Somogyi, Z., Henderson, F.J., Conway, T.C.: Mercury: an efficient purely declarative logic programming language. In: Proceedings of the Australian Computer Science Conference, pp. 499\u2013512 (1995)"},{"key":"11_CR11","doi-asserted-by":"publisher","first-page":"345","DOI":"10.1145\/1167473.1167503","volume-title":"OOPSLA 2006: Proceedings of the 21st annual ACM SIGPLAN conference on Object-oriented programming languages, systems, and applications","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: OOPSLA 2006: Proceedings of the 21st annual ACM SIGPLAN conference on Object-oriented programming languages, systems, and applications, pp. 345\u2013362. ACM Press, New York (2006)"}],"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-642-03359-9_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,9]],"date-time":"2019-03-09T13:28:44Z","timestamp":1552138124000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-03359-9_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642033582","9783642033599"],"references-count":11,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-03359-9_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}