{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T17:26:53Z","timestamp":1725902813860},"publisher-location":"Cham","reference-count":24,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319620749"},{"type":"electronic","value":"9783319620756"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"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":[[2017]]},"DOI":"10.1007\/978-3-319-62075-6_21","type":"book-chapter","created":{"date-parts":[[2017,6,27]],"date-time":"2017-06-27T10:58:50Z","timestamp":1498561130000},"page":"303-318","source":"Crossref","is-referenced-by-count":4,"title":["Proof Mining with Dependent Types"],"prefix":"10.1007","author":[{"given":"Ekaterina","family":"Komendantskaya","sequence":"first","affiliation":[]},{"given":"J\u00f3nathan","family":"Heras","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,6,28]]},"reference":[{"key":"21_CR1","volume-title":"Rippling: Meta-Level Guidance for Mathematical Reasoning","author":"D Basin","year":"2005","unstructured":"Basin, D., et al.: Rippling: Meta-Level Guidance for Mathematical Reasoning. Cambridge University Press, New York (2005)"},{"key":"21_CR2","volume-title":"Pattern Recognition and Machine Learning","author":"C Bishop","year":"2006","unstructured":"Bishop, C.: Pattern Recognition and Machine Learning. Springer, Heidelberg (2006)"},{"issue":"1","key":"21_CR3","first-page":"101","volume":"9","author":"J Blanchette","year":"2016","unstructured":"Blanchette, J., et al.: Hammering towards QED. J. Formalized Reasoning 9(1), 101\u2013148 (2016)","journal-title":"J. Formalized Reasoning"},{"key":"21_CR4","unstructured":"Coq development team. The Coq Proof Assistant Reference Manual, version 8.4pl3. Technical report (2013)"},{"key":"21_CR5","doi-asserted-by":"crossref","unstructured":"Czajka, L., Kaliszyk, C.: Goal translation for a Hammer for Coq. In: Proceeding of Hammers for Type Theories, EPTCS. vol. 210 , pp. 13-20 (2016)","DOI":"10.4204\/EPTCS.210.4"},{"key":"21_CR6","unstructured":"Duncan, H.: The use of Data-Mining for the Automatic Formation of Tactics. Ph.D. thesis, University of Edinburgh (2002)"},{"issue":"2","key":"21_CR7","first-page":"95","volume":"3","author":"G Gonthier","year":"2010","unstructured":"Gonthier, G., Mahboubi, A.: An introduction to small scale reflection. J. Formalized Reasoning 3(2), 95\u2013152 (2010)","journal-title":"J. Formalized Reasoning"},{"key":"21_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"282","DOI":"10.1007\/978-3-319-08434-3_21","volume-title":"Intelligent Computer Mathematics","author":"T Gransden","year":"2014","unstructured":"Gransden, T., Walkinshaw, N., Raman, R.: Mining state-based models from proof corpora. In: Watt, S.M., Davenport, J.H., Sexton, A.P., Sojka, P., Urban, J. (eds.) CICM 2014. LNCS, vol. 8543, pp. 282\u2013297. Springer, Cham (2014). doi: 10.1007\/978-3-319-08434-3_21"},{"key":"21_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"246","DOI":"10.1007\/978-3-319-21401-6_16","volume-title":"Automated Deduction - CADE-25","author":"T Gransden","year":"2015","unstructured":"Gransden, T., Walkinshaw, N., Raman, R.: SEPIA: Search for proofs using inferred automata. In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS, vol. 9195, pp. 246\u2013255. Springer, Cham (2015). doi: 10.1007\/978-3-319-21401-6_16"},{"issue":"1","key":"21_CR10","doi-asserted-by":"crossref","first-page":"10","DOI":"10.1145\/1656274.1656278","volume":"11","author":"M Hall","year":"2009","unstructured":"Hall, M., et al.: The WEKA data mining software: an update. SIGKDD Explor. 11(1), 10\u201318 (2009)","journal-title":"SIGKDD Explor."},{"issue":"4","key":"21_CR11","doi-asserted-by":"crossref","first-page":"26:1","DOI":"10.1145\/2528929","volume":"14","author":"J Heras","year":"2013","unstructured":"Heras, J., et al.: Computing persistent homology within Coq\/SSReflect. ACM Trans. Comput. Logic 14(4), 26:1\u201326:16 (2013)","journal-title":"ACM Trans. Comput. Logic"},{"issue":"1","key":"21_CR12","doi-asserted-by":"crossref","first-page":"99","DOI":"10.1007\/s11786-014-0173-1","volume":"8","author":"J Heras","year":"2014","unstructured":"Heras, J., Komendantskaya, E.: Recycling proof patterns in Coq: case studies. J. Math. Comput. Sci. 8(1), 99\u2013116 (2014)","journal-title":"J. Math. Comput. Sci."},{"key":"21_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"228","DOI":"10.1007\/978-3-642-28717-6_19","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"S Hetzl","year":"2012","unstructured":"Hetzl, S., Leitsch, A., Weller, D.: Towards algorithmic cut-introduction. In: Bj\u00f8rner, N., Voronkov, A. (eds.) LPAR 2012. LNCS, vol. 7180, pp. 228\u2013242. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-28717-6_19"},{"key":"21_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"389","DOI":"10.1007\/978-3-642-45221-5_27","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"J Heras","year":"2013","unstructured":"Heras, J., Komendantskaya, E., Johansson, M., Maclean, E.: Proof-pattern recognition and lemma discovery in ACL2. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) LPAR 2013. LNCS, vol. 8312, pp. 389\u2013406. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-45221-5_27"},{"issue":"3","key":"21_CR15","doi-asserted-by":"crossref","first-page":"251","DOI":"10.1007\/s10817-010-9193-y","volume":"47","author":"M Johansson","year":"2011","unstructured":"Johansson, M., et al.: Conjecture synthesis for inductive theories. J. Autom. Reasoning 47(3), 251\u2013289 (2011)","journal-title":"J. Autom. Reasoning"},{"key":"21_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/978-3-319-08434-3_9","volume-title":"Intelligent Computer Mathematics","author":"M Johansson","year":"2014","unstructured":"Johansson, M., Ros\u00e9n, D., Smallbone, N., Claessen, K.: Hipster: integrating theory exploration in a proof assistant. In: Watt, S.M., Davenport, J.H., Sexton, A.P., Sojka, P., Urban, J. (eds.) CICM 2014. LNCS, vol. 8543, pp. 108\u2013122. Springer, Cham (2014). doi: 10.1007\/978-3-319-08434-3_9"},{"key":"21_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"503","DOI":"10.1007\/978-3-642-45221-5_34","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"C Kaliszyk","year":"2013","unstructured":"Kaliszyk, C., Urban, J.: Lemma mining over HOL Light. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) LPAR 2013. LNCS, vol. 8312, pp. 503\u2013517. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-45221-5_34"},{"key":"21_CR18","doi-asserted-by":"crossref","first-page":"109","DOI":"10.1016\/j.jsc.2014.09.032","volume":"69","author":"C Kaliszyk","year":"2015","unstructured":"Kaliszyk, C., Urban, J.: Learning-assisted theorem proving with millions of lemmas. J. Symb. Comput. 69, 109\u2013128 (2015)","journal-title":"J. Symb. Comput."},{"key":"21_CR19","doi-asserted-by":"crossref","unstructured":"Kaufmann, M., Manolios, P., Moore, P. (eds.): Computer-Aided Reasoning: An Approach. Kluwer Academic Publishers, Boston (2000)","DOI":"10.1007\/978-1-4615-4449-4"},{"key":"21_CR20","doi-asserted-by":"crossref","first-page":"15","DOI":"10.4204\/EPTCS.118.2","volume":"118","author":"E Komendantskaya","year":"2013","unstructured":"Komendantskaya, E., et al.: Machine learning for proof general: interfacing interfaces. Electron. Proc. Theor. Comput. Sci. 118, 15\u201341 (2013)","journal-title":"Electron. Proc. Theor. Comput. Sci."},{"key":"21_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1007\/978-3-642-39634-2_6","volume-title":"Interactive Theorem Proving","author":"D K\u00fchlwein","year":"2013","unstructured":"K\u00fchlwein, D., Blanchette, J.C., Kaliszyk, C., Urban, J.: MaSh: machine learning for sledgehammer. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol. 7998, pp. 35\u201350. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-39634-2_6"},{"key":"21_CR22","unstructured":"The Univalent Foundations Program. Homotopy Type Theory. Institute for Advanced Study. https:\/\/github.com\/HoTT\/HoTT\/wiki (2013)"},{"key":"21_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1007\/978-3-642-03359-9_21","volume-title":"Theorem Proving in Higher Order Logics","author":"S Roux","year":"2009","unstructured":"Roux, S.: Acyclic preferences and existence of sequential nash equilibria: a formal and constructive equivalence. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 293\u2013309. Springer, Heidelberg (2009). doi: 10.1007\/978-3-642-03359-9_21"},{"issue":"2","key":"21_CR24","doi-asserted-by":"crossref","first-page":"229","DOI":"10.1007\/s10817-012-9269-y","volume":"50","author":"J Urban","year":"2013","unstructured":"Urban, J., et al.: ATP and presentation service for Mizar formalizations. J. Autom. Reasoning 50(2), 229\u2013241 (2013)","journal-title":"J. Autom. Reasoning"}],"container-title":["Lecture Notes in Computer Science","Intelligent Computer Mathematics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-62075-6_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,27]],"date-time":"2019-09-27T02:27:01Z","timestamp":1569551221000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-62075-6_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319620749","9783319620756"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-62075-6_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}