{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,7]],"date-time":"2026-10-07T00:20:20Z","timestamp":1791332420745,"version":"4.3.1"},"publisher-location":"Berlin, Heidelberg","reference-count":8,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540556022","type":"print"},{"value":"9783540472520","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1992]]},"DOI":"10.1007\/3-540-55602-8_201","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T05:21:27Z","timestamp":1330233687000},"page":"673-676","source":"Crossref","is-referenced-by-count":18,"title":["Isabelle-91"],"prefix":"10.1007","author":[{"given":"Tobias","family":"Nipkow","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Lawrence C.","family":"Paulson","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2005,6,8]]},"reference":[{"key":"51_CR1","doi-asserted-by":"crossref","first-page":"27","DOI":"10.1016\/0304-3975(75)90011-0","volume":"1","author":"G. Huet","year":"1975","unstructured":"G. Huet. A unification algorithm for typed \u03bb-calculus. Theoretical Computer Science, 1:27\u201357, 1975.","journal-title":"Theoretical Computer Science"},{"key":"51_CR2","unstructured":"R. Milwer, M. Tofte, and R. Harper. The Definition of Standard ML. MIT Press, 1990."},{"key":"51_CR3","unstructured":"T. Nipkow. Order-sorted polymorphism in isabelle. In G. Huet, G. Plotkin, and C. Jones, editors, Proc. 2nd Workshop on Logical Frameworks, pages 307\u2013321, 1991."},{"key":"51_CR4","doi-asserted-by":"crossref","unstructured":"T. Nipkow and G. Snelting. Type classes and overloading resolution via order-sorted unification. In Proc. 5th ACM Conf. Functional Programming Languages and Computer Architecture, pages 1\u201314. LNCS 523, 1991.","DOI":"10.1007\/3540543961_1"},{"key":"51_CR5","doi-asserted-by":"crossref","first-page":"363","DOI":"10.1007\/BF00248324","volume":"5","author":"L. C. Paulson","year":"1989","unstructured":"L. C. Paulson. The foundation of a generic theorem prover. J. Automated Reasoning, 5:363\u2013397, 1989.","journal-title":"J. Automated Reasoning"},{"key":"51_CR6","unstructured":"L. C. Paulson. Isabelle: The next 700 theorem provers. In P. Odifreddi, editor, Logic and Computer Science, pages 361\u2013385. Academic Press, 1990."},{"key":"51_CR7","unstructured":"L. C. Paulson and T. Nipkow. Isabelle tutorial and user's manual. Technical Report 189, University of Cambridge, Computer Laboratory, 1990."},{"key":"51_CR8","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1007\/BF02432151","volume":"2","author":"F. J. Pelletier","year":"1986","unstructured":"F. J. Pelletier. Seventy-five problems for testing automatic theorem provers. J. Automated Reasoning, 2:191\u2013216, 1986. Errata, JAR 4 (1988), 236\u2013236.","journal-title":"J. Automated Reasoning"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction\u2014CADE-11"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-55602-8_201.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T21:32:59Z","timestamp":1619559179000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-55602-8_201"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1992]]},"ISBN":["9783540556022","9783540472520"],"references-count":8,"URL":"https:\/\/doi.org\/10.1007\/3-540-55602-8_201","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1992]]}}}