{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T10:09:27Z","timestamp":1742983767923,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":12,"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_18","type":"book-chapter","created":{"date-parts":[[2009,8,19]],"date-time":"2009-08-19T21:46:12Z","timestamp":1250718372000},"page":"244-259","source":"Crossref","is-referenced-by-count":15,"title":["The HOL-Omega Logic"],"prefix":"10.1007","author":[{"given":"Peter V.","family":"Homeier","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"18_CR1","doi-asserted-by":"crossref","unstructured":"Bird, R., de Moor, O.: Algebra of Programming. Prentice Hall (1997)","DOI":"10.1007\/978-3-642-61455-2_12"},{"key":"18_CR2","first-page":"555","volume-title":"Proceedings 9th Int. Congress of Logic, Methodology and Philosophy of Science","author":"T. Coquand","year":"1994","unstructured":"Coquand, T.: A new paradox in type theory. In: Prawitx, D., Skyrms, B., Westerstahl, D. (eds.) Proceedings 9th Int. Congress of Logic, Methodology and Philosophy of Science, pp. 555\u2013570. North-Holland, Amsterdam (1994)"},{"key":"18_CR3","volume-title":"Introduction to HOL","author":"M.J.C. Gordon","year":"1993","unstructured":"Gordon, M.J.C., Melham, T.F.: Introduction to HOL. Cambridge University Press, Cambridge (1993)"},{"key":"18_CR4","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1016\/B978-0-444-89901-9.50012-4","volume-title":"Towards Verified Systems, ch.\u00a03","author":"M.J.C. Gordon","year":"1994","unstructured":"Gordon, M.J.C., Pitts, A.M.: The HOL Logic and System. In: Bowen, J. (ed.) Towards Verified Systems, ch.\u00a03, pp. 49\u201370. Elsevier Science B.V., Amsterdam (1994)"},{"key":"18_CR5","unstructured":"The HOL System DESCRIPTION (Version Kananaskis 4), \n                    \n                      http:\/\/downloads.sourceforge.net\/hol\/kananaskis-4-description.pdf"},{"key":"18_CR6","unstructured":"The HOL System LOGIC (Version Kananaskis 4), \n                    \n                      http:\/\/downloads.sourceforge.net\/hol\/kananaskis-4-logic.pdf"},{"key":"18_CR7","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1016\/S0022-4049(02)00137-8","volume":"175","author":"S. Lack","year":"2002","unstructured":"Lack, S., Street, R.: The formal theory of monads II. Journal of Pure Applied Algorithms\u00a0175, 243\u2013265 (2002)","journal-title":"Journal of Pure Applied Algorithms"},{"issue":"1-2","key":"18_CR8","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1007\/BF01383982","volume":"3","author":"T.F. Melham","year":"1993","unstructured":"Melham, T.F.: The HOL Logic Extended with Quantification over Type Variables. Formal Methods in System Design\u00a03(1-2), 7\u201324 (1993)","journal-title":"Formal Methods in System Design"},{"key":"18_CR9","volume-title":"Introduction to Set Theory","author":"J.D. Monk","year":"1969","unstructured":"Monk, J.D.: Introduction to Set Theory. McGraw-Hill, New York (1969)"},{"key":"18_CR10","volume-title":"Types and Programming Languages","author":"B.C. Pierce","year":"2002","unstructured":"Pierce, B.C.: Types and Programming Languages. MIT Press, Cambridge (2002)"},{"key":"18_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"334","DOI":"10.1007\/978-3-540-74591-4_25","volume-title":"Theorem Proving in Higher Order Logics","author":"N. V\u00f6lker","year":"2007","unstructured":"V\u00f6lker, N.: HOL2P - A System of Classical Higher Order Logic with Second Order Polymorphism. In: Schneider, K., Brandt, J. (eds.) TPHOLs 2007. LNCS, vol.\u00a04732, pp. 334\u2013351. Springer, Heidelberg (2007)"},{"key":"18_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-59451-5_2","volume-title":"Advanced Functional Programming","author":"P. Wadler","year":"1995","unstructured":"Wadler, P.: Monads for functional programming. In: Jeuring, J., Meijer, E. (eds.) AFP 1995. LNCS, vol.\u00a0925. Springer, Heidelberg (1995)"}],"container-title":["Lecture Notes in Computer Science","Theorem Proving in Higher Order Logics"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-03359-9_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T12:13:33Z","timestamp":1558268013000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-03359-9_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642033582","9783642033599"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-03359-9_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}