{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,15]],"date-time":"2026-01-15T01:35:12Z","timestamp":1768440912718,"version":"3.49.0"},"publisher-location":"Cham","reference-count":9,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319968117","type":"print"},{"value":"9783319968124","type":"electronic"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","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":[[2018]]},"DOI":"10.1007\/978-3-319-96812-4_5","type":"book-chapter","created":{"date-parts":[[2018,7,17]],"date-time":"2018-07-17T04:26:41Z","timestamp":1531801601000},"page":"53-59","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Concrete Semantics with Coq and CoqHammer"],"prefix":"10.1007","author":[{"given":"\u0141ukasz","family":"Czajka","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Burak","family":"Ekici","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8273-6059","authenticated-orcid":false,"given":"Cezary","family":"Kaliszyk","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,7,18]]},"reference":[{"issue":"3","key":"5_CR1","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1007\/s10817-016-9362-8","volume":"57","author":"JC Blanchette","year":"2016","unstructured":"Blanchette, J.C., Greenaway, D., Kaliszyk, C., K\u00fchlwein, D., Urban, J.: A learning-based fact selector for Isabelle\/HOL. J. Autom. Reason. 57(3), 219\u2013244 (2016)","journal-title":"J. Autom. Reason."},{"key":"5_CR2","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/9153.001.0001","volume-title":"Certified Programming with Dependent Types - A Pragmatic Introduction to the Coq Proof Assistant","author":"A Chlipala","year":"2013","unstructured":"Chlipala, A.: Certified Programming with Dependent Types - A Pragmatic Introduction to the Coq Proof Assistant. MIT Press, Cambridge (2013)"},{"key":"5_CR3","doi-asserted-by":"publisher","first-page":"13","DOI":"10.4204\/EPTCS.210.4","volume":"210","author":"\u0141ukasz Czajka","year":"2016","unstructured":"Czajka, \u0141., Kaliszyk, C.: Goal translation for a hammer for Coq (extended abstract). In: Blanchette, J., Kaliszyk, C. (eds.) International Workshop on Hammers for Type Theories (HaTT 2016). EPTCS, vol. 210, pp. 13\u201320 (2016)","journal-title":"Electronic Proceedings in Theoretical Computer Science"},{"key":"5_CR4","doi-asserted-by":"crossref","unstructured":"Dong, D., Wu, H., He, W., Yu, D., Wang, H.: Multi-task learning for multiple language translation. In: ACL, no. 1, pp. 1723\u20131732. The Association for Computer Linguistics (2015)","DOI":"10.3115\/v1\/P15-1166"},{"key":"5_CR5","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"435","DOI":"10.1007\/978-3-319-08434-3_34","volume-title":"Intelligent Computer Mathematics","author":"C Kaliszyk","year":"2014","unstructured":"Kaliszyk, C., Urban, J., Vysko\u010dil, J., Geuvers, H.: Developing corpus-based translation methods between informal and formal mathematics: project description. In: Watt, S.M., Davenport, J.H., Sexton, A.P., Sojka, P., Urban, J. (eds.) CICM 2014. LNCS (LNAI), vol. 8543, pp. 435\u2013439. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08434-3_34"},{"key":"5_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-39799-8_1","volume-title":"Computer Aided Verification","author":"L Kov\u00e1cs","year":"2013","unstructured":"Kov\u00e1cs, L., Voronkov, A.: First-order theorem proving and Vampire. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 1\u201335. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_1"},{"key":"5_CR7","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10542-0","volume-title":"Concrete Semantics - With Isabelle\/HOL","author":"T Nipkow","year":"2014","unstructured":"Nipkow, T., Klein, G.: Concrete Semantics - With Isabelle\/HOL. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-10542-0"},{"key":"5_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"735","DOI":"10.1007\/978-3-642-45221-5_49","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"S Schulz","year":"2013","unstructured":"Schulz, S.: System description: E 1.8. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) LPAR 2013. LNCS, vol. 8312, pp. 735\u2013743. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-45221-5_49"},{"issue":"1\u20134","key":"5_CR9","doi-asserted-by":"publisher","first-page":"423","DOI":"10.1007\/s10817-018-9458-4","volume":"61","author":"\u0141 Czajka","year":"2018","unstructured":"Czajka, \u0141., Kaliszyk, C.: Hammer for Coq: automation for dependent type theory. J. Autom. Reason. 61(1\u20134), 423\u2013453 (2018)","journal-title":"J. Autom. Reason."}],"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-96812-4_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,20]],"date-time":"2019-10-20T18:30:11Z","timestamp":1571596211000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-96812-4_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319968117","9783319968124"],"references-count":9,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-96812-4_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018]]}}}