{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T04:23:37Z","timestamp":1742963017514,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":10,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642228629"},{"type":"electronic","value":"9783642228636"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"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":[[2011]]},"DOI":"10.1007\/978-3-642-22863-6_28","type":"book-chapter","created":{"date-parts":[[2011,8,8]],"date-time":"2011-08-08T05:47:55Z","timestamp":1312782475000},"page":"370-375","source":"Crossref","is-referenced-by-count":3,"title":["Composable Discovery Engines for Interactive Theorem Proving"],"prefix":"10.1007","author":[{"given":"Phil","family":"Scott","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jacques","family":"Fleuriot","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"28_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/BFb0031814","volume-title":"Formal Methods in Computer-Aided Design","author":"J. Harrison","year":"1996","unstructured":"Harrison, J.: HOL Light: a Tutorial Introduction. In: Srivas, M., Camilleri, A. (eds.) FMCAD 1996. LNCS, vol.\u00a01166, pp. 265\u2013269. Springer, Heidelberg (1996)"},{"key":"28_CR2","unstructured":"Hilbert, D.: Foundations of Geometry. Open Court Classics, 10th edn. (1971)"},{"issue":"1","key":"28_CR3","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1017\/S0956796807006326","volume":"18","author":"C. McBride","year":"2008","unstructured":"McBride, C., Paterson, R.: Applicative programming with effects. Journal of Functional Programming\u00a018(1), 1\u201313 (2008)","journal-title":"Journal of Functional Programming"},{"issue":"10","key":"28_CR4","doi-asserted-by":"publisher","first-page":"1575","DOI":"10.1016\/j.ic.2005.05.010","volume":"204","author":"J. Meng","year":"2006","unstructured":"Meng, J., Quigley, C., Paulson, L.C.: Automation for interactive proof: First prototype. Inf. Comput.\u00a0204(10), 1575\u20131596 (2006)","journal-title":"Inf. Comput."},{"key":"28_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0030541","volume-title":"Isabelle: a Generic Theorem Prover","author":"L.C. Paulson","year":"1994","unstructured":"Paulson, L.C.: Isabelle: a Generic Theorem Prover. LNCS, vol.\u00a0828. Springer, Heidelberg (1994)"},{"key":"28_CR6","unstructured":"Sam Lindley, J.Y., Wadler, P.: Idioms are oblivious, arrows are meticulous, monads are promiscuous. In: Mathematically Structured Functional Programming (2008), \n                    \n                      http:\/\/hdl.handle.net\/1842\/3800"},{"key":"28_CR7","unstructured":"Scott, P.: Mechanising Hilbert\u2019s Foundations of Geometry in Isabelle. Master\u2019s thesis, University of Edinburgh (2008)"},{"issue":"3-4","key":"28_CR8","doi-asserted-by":"publisher","first-page":"469","DOI":"10.1017\/S0956796809007321","volume":"19","author":"J.M. Spivey","year":"2009","unstructured":"Spivey, J.M.: Algebras for combinatorial search. Journal of Functional Programming\u00a019(3-4), 469\u2013487 (2009)","journal-title":"Journal of Functional Programming"},{"key":"28_CR9","doi-asserted-by":"crossref","unstructured":"Wadler, P.: Monads for functional programming. In: Advanced Functional Programming, pp. 24\u201352 (1995)","DOI":"10.1007\/3-540-59451-5_2"},{"key":"28_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"378","DOI":"10.1007\/3-540-44755-5_26","volume-title":"Theorem Proving in Higher Order Logics","author":"F. Wiedijk","year":"2001","unstructured":"Wiedijk, F.: Mizar Light for HOL Light. In: Boulton, R.J., Jackson, P.B. (eds.) TPHOLs 2001. LNCS, vol.\u00a02152, pp. 378\u2013394. Springer, Heidelberg (2001)"}],"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-22863-6_28","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,31]],"date-time":"2019-03-31T02:27:55Z","timestamp":1553999275000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-22863-6_28"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642228629","9783642228636"],"references-count":10,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-22863-6_28","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}