{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T18:01:00Z","timestamp":1725559260616},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642140518"},{"type":"electronic","value":"9783642140525"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-14052-5_23","type":"book-chapter","created":{"date-parts":[[2010,7,12]],"date-time":"2010-07-12T14:23:14Z","timestamp":1278944594000},"page":"323-338","source":"Crossref","is-referenced-by-count":17,"title":["A Mechanized Translation from Higher-Order Logic to Set Theory"],"prefix":"10.1007","author":[{"given":"Alexander","family":"Krauss","sequence":"first","affiliation":[]},{"given":"Andreas","family":"Schropp","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"23_CR1","first-page":"1","volume":"13","author":"M. Bortin","year":"2006","unstructured":"Bortin, M., Broch Johnsen, E., L\u00fcth, C.: Structured formal development in Isabelle. Nordic Journal of Computing\u00a013, 1\u201320 (2006)","journal-title":"Nordic Journal of Computing"},{"issue":"2-3","key":"23_CR2","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1016\/0890-5401(88)90005-3","volume":"76","author":"T. Coquand","year":"1988","unstructured":"Coquand, T., Huet, G.: The calculus of constructions. Information and Computation\u00a076(2-3), 95\u2013120 (1988)","journal-title":"Information and Computation"},{"key":"23_CR3","series-title":"Lecture Notes in Artificial Intelligence","volume-title":"Automated Reasoning","year":"2006","unstructured":"Furbach, U., Shankar, N. (eds.): IJCAR 2006. LNCS (LNAI), vol.\u00a04130. Springer, Heidelberg (2006)"},{"issue":"3-4","key":"23_CR4","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1007\/BF02761593","volume":"22","author":"H. Gaifman","year":"1975","unstructured":"Gaifman, H.: Global and local choice functions. Israel Journal of Mathematics\u00a022(3-4), 257\u2013265 (1975)","journal-title":"Israel Journal of Mathematics"},{"key":"23_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1007\/BFb0105405","volume-title":"Theorem Proving in Higher Order Logics","author":"M.J.C. Gordon","year":"1996","unstructured":"Gordon, M.J.C.: Set theory, higher order logic or both? In: von Wright, J., Harrison, J., Grundy, J. (eds.) TPHOLs 1996. LNCS, vol.\u00a01125, pp. 191\u2013201. Springer, Heidelberg (1996)"},{"key":"23_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-71067-7_1","volume-title":"Theorem Proving in Higher Order Logics","author":"M.J.C. Gordon","year":"2008","unstructured":"Gordon, M.J.C.: Twenty years of theorem proving for HOLs: Past, present and future. In: Ait Mohamed, O., Mu\u00f1oz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol.\u00a05170, pp. 1\u20135. Springer, Heidelberg (2008)"},{"key":"23_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"160","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, pp. 160\u2013174. Springer, Heidelberg (2007)"},{"key":"23_CR8","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 (TPHOLs 2009)","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)"},{"issue":"3","key":"23_CR9","doi-asserted-by":"publisher","first-page":"502","DOI":"10.1145\/319301.319317","volume":"21","author":"L. Lamport","year":"1999","unstructured":"Lamport, L., Paulson, L.C.: Should your specification language be typed? ACM Transactions on Programming Languages and Systems\u00a021(3), 502\u2013526 (1999)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"23_CR10","doi-asserted-by":"crossref","unstructured":"McLaughlin, S.: An interpration of Isabelle\/HOL in HOL Light. In: Furbach, Shankar: [3], pp. 192\u2013204","DOI":"10.1007\/11814771_18"},{"key":"23_CR11","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4757-4153-7","volume-title":"Notes on Set Theory","author":"Y.N. Moschovakis","year":"1994","unstructured":"Moschovakis, Y.N.: Notes on Set Theory. Springer, Heidelberg (1994)"},{"issue":"2","key":"23_CR12","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(2), 191\u2013223 (1999)","journal-title":"Journal of Functional Programming"},{"key":"23_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"212","DOI":"10.1007\/11805618_16","volume-title":"Term Rewriting and Applications","author":"S. Obua","year":"2006","unstructured":"Obua, S.: Checking conservativity of overloaded definitions in higher-order logic. In: Pfenning, F. (ed.) RTA 2006. LNCS, vol.\u00a04098, pp. 212\u2013226. Springer, Heidelberg (2006)"},{"key":"23_CR14","doi-asserted-by":"crossref","unstructured":"Obua, S., Skalberg, S.: Importing HOL into Isabelle\/HOL. In: Furbach, Shankar: [3], pp. 298\u2013302","DOI":"10.1007\/11814771_27"},{"key":"23_CR15","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/BF00248324","volume":"5","author":"L.C. Paulson","year":"1989","unstructured":"Paulson, L.C.: The foundation of a generic theorem prover. Journal of Automated Reasoning\u00a05, 363\u2013397 (1989)","journal-title":"Journal of Automated Reasoning"},{"key":"23_CR16","doi-asserted-by":"publisher","first-page":"353","DOI":"10.1007\/BF00881873","volume":"11","author":"L.C. Paulson","year":"1993","unstructured":"Paulson, L.C.: Set theory for verification: I. From foundations to functions. Journal of Automated Reasoning\u00a011, 353\u2013389 (1993)","journal-title":"Journal of Automated Reasoning"},{"key":"23_CR17","first-page":"191","volume-title":"Introduction to HOL: A theorem proving environment for Higher Order Logic","author":"A. Pitts","year":"1993","unstructured":"Pitts, A.: The HOL logic. In: Gordon, M., Melham, T. (eds.) Introduction to HOL: A theorem proving environment for Higher Order Logic, pp. 191\u2013232. Cambridge University Press, Cambridge (1993)"},{"key":"23_CR18","series-title":"Lecture Notes in Computer Science","volume-title":"Computational Aspects of an Order-Sorted Logic with Term Declarations","year":"1989","unstructured":"Schmidt-Schau\u00df, M. (ed.): Computational Aspects of an Order-Sorted Logic with Term Declarations. LNCS, vol.\u00a0395. Springer, Heidelberg (1989)"},{"key":"23_CR19","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":"23_CR20","unstructured":"Wiedijk, F.: The QED manifesto revisited. In: Matuszewski, R., Zalewska, A. (eds.) From Insight To Proof \u2013 Festschrift in Honour of Andrzej Trybulec, pp. 121\u2013133. University of Bia\u0142ystok (2007)"}],"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-14052-5_23.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,24]],"date-time":"2020-11-24T02:47:02Z","timestamp":1606186022000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-14052-5_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642140518","9783642140525"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-14052-5_23","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}