{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T09:17:38Z","timestamp":1742980658310,"version":"3.40.3"},"publisher-location":"Cham","reference-count":14,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319206141"},{"type":"electronic","value":"9783319206158"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-20615-8_6","type":"book-chapter","created":{"date-parts":[[2015,6,22]],"date-time":"2015-06-22T15:31:23Z","timestamp":1434987083000},"page":"87-101","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Type Inference for ZFH"],"prefix":"10.1007","author":[{"given":"Steven","family":"Obua","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jacques","family":"Fleuriot","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Phil","family":"Scott","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David","family":"Aspinall","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,6,23]]},"reference":[{"key":"6_CR1","unstructured":"ProofPeer. http:\/\/www.proofpeer.net"},{"key":"6_CR2","unstructured":"Obua, S., Fleuriot, J., Scott, P., Aspinall, D.: ProofPeer: Collaborative Theorem Proving. http:\/\/arxiv.org\/abs\/1404.6186"},{"key":"6_CR3","unstructured":"Hales, T., et al.: A formal proof of the Kepler conjecture. http:\/\/arxiv.org\/abs\/1501.02155"},{"key":"6_CR4","unstructured":"Homotopy Type Theory. http:\/\/homotopytypetheory.org\/"},{"key":"6_CR5","series-title":"Lecture Notes in Computer Science","volume-title":"Higher Order Logic Theorem Proving and Its Applications","author":"S Agerholm","year":"1995","unstructured":"Agerholm, S., Gordon, M.: Experiments with ZF set theory in HOL and Isabelle. In: Schubert, E.T., Alves-Foss, J., Windley, P. (eds.) HUG 1995. LNCS, vol. 971. Springer, Heidelberg (1995)"},{"key":"6_CR6","series-title":"Lecture Notes in Computer Science","volume-title":"Theorem Proving in Higher Order Logics","author":"M Gordon","year":"1996","unstructured":"Gordon, M.: Set theory, higher order logic or both? In: von Wright, J., Harrison, J., Grundy, J. (eds.) TPHOLs 1996. LNCS, vol. 1125. Springer, Heidelberg (1996)"},{"issue":"3","key":"6_CR7","doi-asserted-by":"publisher","first-page":"353","DOI":"10.1007\/BF00881873","volume":"11","author":"LC Paulson","year":"1993","unstructured":"Paulson, L.C.: Set theory for verification: I. from foundations to functions. J. Autom. Reasoning 11(3), 353\u2013389 (1993). Springer","journal-title":"J. Autom. Reasoning"},{"issue":"4","key":"6_CR8","doi-asserted-by":"publisher","first-page":"303","DOI":"10.1007\/s10817-009-9157-2","volume":"44","author":"A Krauss","year":"2010","unstructured":"Krauss, A.: Partial and nested recursive function definitions in higher-order logic. J. Autom. Reasoning 44(4), 303\u2013336 (2010). Springer","journal-title":"J. Autom. Reasoning"},{"key":"6_CR9","unstructured":"ProofPeer Root Theory. http:\/\/proofpeer.net\/repository?root.thy"},{"key":"6_CR10","volume-title":"Term Rewriting and All That","author":"F Baader","year":"1999","unstructured":"Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1999)"},{"key":"6_CR11","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1016\/0022-0000(78)90014-4","volume":"17","author":"R Milner","year":"1978","unstructured":"Milner, R.: A theory of type polymorphism in programming. J. Comput. Syst. Sci. 17, 348\u2013375 (1978)","journal-title":"J. Comput. Syst. Sci."},{"key":"6_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1007\/978-3-642-25318-8_10","volume-title":"Programming Languages and Systems","author":"D Traytel","year":"2011","unstructured":"Traytel, D., Berghofer, S., Nipkow, T.: Extending hindley-milner type inference with coercive structural subtyping. In: Yang, H. (ed.) APLAS 2011. LNCS, vol. 7078, pp. 89\u2013104. Springer, Heidelberg (2011)"},{"issue":"04","key":"6_CR13","doi-asserted-by":"publisher","first-page":"729","DOI":"10.1017\/S0960129508006804","volume":"18","author":"Z Luo","year":"2008","unstructured":"Luo, Z.: Coercions in a polymorphic type system. Math. Struct. Comput. Sci. 18(04), 729\u2013751 (2008). Cambridge Journals","journal-title":"Math. Struct. Comput. Sci."},{"key":"6_CR14","doi-asserted-by":"crossref","unstructured":"Odersky, M., Wadler, P., Wehr, M.: A second look at overloading. In: Proceedings of the Seventh International Conference on Functional Programming Languages and Computer Architecture. ACM (1995)","DOI":"10.1145\/224164.224195"}],"container-title":["Lecture Notes in Computer Science","Intelligent Computer Mathematics"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-20615-8_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,28]],"date-time":"2023-01-28T12:08:59Z","timestamp":1674907739000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-20615-8_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319206141","9783319206158"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-20615-8_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"23 June 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}