{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,5]],"date-time":"2025-11-05T06:39:16Z","timestamp":1762324756240,"version":"3.40.3"},"publisher-location":"Cham","reference-count":75,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030510534"},{"type":"electronic","value":"9783030510541"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"vor","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":[[2020]]},"DOI":"10.1007\/978-3-030-51054-1_6","type":"book-chapter","created":{"date-parts":[[2020,6,29]],"date-time":"2020-06-29T19:02:39Z","timestamp":1593457359000},"page":"97-118","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Deep Generation of Coq Lemma Names Using Elaborated Terms"],"prefix":"10.1007","author":[{"given":"Pengyu","family":"Nie","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Karl","family":"Palmskog","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Junyi Jessy","family":"Li","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Milos","family":"Gligoric","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2020,6,24]]},"reference":[{"key":"6_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1007\/978-3-319-22102-1_2","volume-title":"Interactive Theorem Proving","author":"R Affeldt","year":"2015","unstructured":"Affeldt, R., Garrigue, J.: Formalization of error-correcting codes: from Hamming to modern coding theory. In: Urban, C., Zhang, X. (eds.) ITP 2015. LNCS, vol. 9236, pp. 17\u201333. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-22102-1_2"},{"key":"6_CR2","doi-asserted-by":"publisher","unstructured":"Allamanis, M., Barr, E.T., Bird, C., Sutton, C.: Learning natural coding conventions. In: International Symposium on the Foundations of Software Engineering, pp. 281\u2013293. ACM, New York (2014). https:\/\/doi.org\/10.1145\/2635868.2635883","DOI":"10.1145\/2635868.2635883"},{"key":"6_CR3","doi-asserted-by":"publisher","unstructured":"Allamanis, M., Barr, E.T., Bird, C., Sutton, C.: Suggesting accurate method and class names. In: Joint Meeting on Foundations of Software Engineering, pp. 38\u201349. ACM, New York (2015). https:\/\/doi.org\/10.1145\/2786805.2786849","DOI":"10.1145\/2786805.2786849"},{"issue":"4","key":"6_CR4","doi-asserted-by":"publisher","first-page":"81:3","DOI":"10.1145\/3212695","volume":"51","author":"M Allamanis","year":"2018","unstructured":"Allamanis, M., Barr, E.T., Devanbu, P., Sutton, C.: A survey of machine learning for big code and naturalness. ACM Comput. Surv. 51(4), 81:3\u201381:37 (2018). https:\/\/doi.org\/10.1145\/3212695","journal-title":"ACM Comput. Surv."},{"key":"6_CR5","unstructured":"Allamanis, M., Peng, H., Sutton, C.: A convolutional attention network for extreme summarization of source code. In: International Conference on Machine Learning, pp. 2091\u20132100 (2016)"},{"key":"6_CR6","unstructured":"Apache Software Foundation: Apache Lucene (2020). https:\/\/lucene.apache.org . Accessed 23 Jan 2020"},{"key":"6_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"459","DOI":"10.1007\/978-3-319-43144-4_28","volume-title":"Interactive Theorem Proving","author":"D Aspinall","year":"2016","unstructured":"Aspinall, D., Kaliszyk, C.: What\u2019s in a theorem name? In: Blanchette, J.C., Merz, S. (eds.) ITP 2016. LNCS, vol. 9807, pp. 459\u2013465. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-43144-4_28"},{"key":"6_CR8","doi-asserted-by":"publisher","unstructured":"Avidan, E., Feitelson, D.G.: Effects of variable names on comprehension: an empirical study. In: International Conference on Program Comprehension, pp. 55\u201365. IEEE Computer Society, Washington (2017). https:\/\/doi.org\/10.1109\/ICPC.2017.27","DOI":"10.1109\/ICPC.2017.27"},{"key":"6_CR9","unstructured":"Avigad, J.: Mathlib naming conventions (2016). https:\/\/github.com\/leanprover-community\/mathlib\/blob\/snapshot-2019-10\/docs\/contribute\/naming.md . Accessed 23 Jan 2020"},{"key":"6_CR10","unstructured":"Babii, H., Janes, A., Robbes, R.: Modeling vocabulary for big code machine learning. CoRR abs\/1904.01873 (2019). https:\/\/arxiv.org\/abs\/1904.01873"},{"key":"6_CR11","unstructured":"Bahdanau, D., Cho, K., Bengio, Y.: Neural machine translation by jointly learning to align and translate. In: International Conference on Learning Representations (2015). https:\/\/arxiv.org\/abs\/1409.0473"},{"issue":"3","key":"6_CR12","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1023\/A:1015761529444","volume":"28","author":"H Barendregt","year":"2002","unstructured":"Barendregt, H., Barendsen, E.: Autarkic computations in formal proofs. J. Autom. Reason. 28(3), 321\u2013336 (2002). https:\/\/doi.org\/10.1023\/A:1015761529444","journal-title":"J. Autom. Reason."},{"key":"6_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/978-3-319-08970-6_6","volume-title":"Interactive Theorem Proving","author":"E-I Bartzia","year":"2014","unstructured":"Bartzia, E.-I., Strub, P.-Y.: A formal library for elliptic curves in the Coq proof assistant. In: Klein, G., Gamboa, R. (eds.) ITP 2014. LNCS, vol. 8558, pp. 77\u201392. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08970-6_6"},{"key":"6_CR14","unstructured":"Berg-Kirkpatrick, T., Burkett, D., Klein, D.: An empirical investigation of statistical significance in NLP. In: Joint Conference on Empirical Methods in Natural Language Processing and Computational Natural Language Learning, pp. 995\u20131005. Association for Computational Linguistics, Stroudsburg (2012)"},{"key":"6_CR15","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-07964-5","volume-title":"Interactive Theorem Proving and Program Development: Coq\u2019Art: The Calculus of Inductive Constructions","author":"Y Bertot","year":"2004","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development: Coq\u2019Art: The Calculus of Inductive Constructions. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-662-07964-5"},{"key":"6_CR16","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-319-20615-8_1","volume-title":"Intelligent Computer Mathematics","author":"JC Blanchette","year":"2015","unstructured":"Blanchette, J.C., Haslbeck, M., Matichuk, D., Nipkow, T.: Mining the archive of formal proofs. In: Kerber, M., Carette, J., Kaliszyk, C., Rabe, F., Sorge, V. (eds.) CICM 2015. LNCS (LNAI), vol. 9150, pp. 3\u201317. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-20615-8_1"},{"key":"6_CR17","doi-asserted-by":"publisher","unstructured":"Boogerd, C., Moonen, L.: Evaluating the relation between coding standard violations and faults within and across software versions. In: International Working Conference on Mining Software Repositories, pp. 41\u201350. IEEE Computer Society, Washington (2009). https:\/\/doi.org\/10.1109\/MSR.2009.5069479","DOI":"10.1109\/MSR.2009.5069479"},{"key":"6_CR18","doi-asserted-by":"publisher","unstructured":"Chen, H., Ziegler, D., Chajed, T., Chlipala, A., Kaashoek, M.F., Zeldovich, N.: Using crash Hoare logic for certifying the FSCQ file system. In: Symposium on Operating Systems Principles, pp. 18\u201337. ACM, New York (2015). https:\/\/doi.org\/10.1145\/2815400.2815402","DOI":"10.1145\/2815400.2815402"},{"key":"6_CR19","unstructured":"Cohen, C.: Contribution guide for the Mathematical Components library (2018). https:\/\/github.com\/math-comp\/math-comp\/blob\/mathcomp-1.9.0\/CONTRIBUTING.md . Accessed 14 Apr 2020"},{"key":"6_CR20","doi-asserted-by":"publisher","unstructured":"Coq Development Team: The Coq proof assistant, version 8.10.0, October 2019. https:\/\/doi.org\/10.5281\/zenodo.3476303","DOI":"10.5281\/zenodo.3476303"},{"key":"6_CR21","unstructured":"Coq Development Team: The Gallina specification language (2019). https:\/\/coq.inria.fr\/distrib\/V8.10.2\/refman\/language\/gallina-specification-language.html . Accessed 17 Apr 2020"},{"key":"6_CR22","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/3-540-44404-1_7","volume-title":"Logic for Programming and Automated Reasoning","author":"D Delahaye","year":"2000","unstructured":"Delahaye, D.: A tactic language for the system Coq. In: Parigot, M., Voronkov, A. (eds.) LPAR 2000. LNAI, vol. 1955, pp. 85\u201395. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/3-540-44404-1_7"},{"key":"6_CR23","unstructured":"Doczkal, C., Kaiser, J.O., Smolka, G.: Regular language representations in Coq (2020). https:\/\/github.com\/coq-community\/reglang . Accessed 09 Apr 2020"},{"issue":"1","key":"6_CR24","doi-asserted-by":"publisher","first-page":"521","DOI":"10.1007\/s10817-018-9460-x","volume":"61","author":"C Doczkal","year":"2018","unstructured":"Doczkal, C., Smolka, G.: Regular language representations in the constructive type theory of Coq. J. Autom. Reason. 61(1), 521\u2013553 (2018)","journal-title":"J. Autom. Reason."},{"key":"6_CR25","unstructured":"Eberl, M., Klein, G., Nipkow, T., Paulson, L., Thiemann, R.: Archive of Formal Proofs (2020). https:\/\/www.isa-afp.org . Accessed 23 Jan 2020"},{"key":"6_CR26","unstructured":"Gallego Arias, E.J.: SerAPI: machine-friendly, data-centric serialization for Coq. Technical report, MINES ParisTech (2016). https:\/\/hal-mines-paristech.archives-ouvertes.fr\/hal-01384408"},{"key":"6_CR27","doi-asserted-by":"publisher","unstructured":"Gao, S., Chen, C., Xing, Z., Ma, Y., Song, W., Lin, S.: A neural model for method name generation from functional description. In: International Conference on Software Analysis, Evolution and Reengineering, pp. 414\u2013421. IEEE Computer Society, Washington (2019). https:\/\/doi.org\/10.1109\/SANER.2019.8667994","DOI":"10.1109\/SANER.2019.8667994"},{"issue":"11","key":"6_CR28","first-page":"1382","volume":"55","author":"G Gonthier","year":"2008","unstructured":"Gonthier, G.: Formal proof\u2013the four-color theorem. Not. Am. Math. Soc. 55(11), 1382\u20131393 (2008)","journal-title":"Not. Am. Math. Soc."},{"key":"6_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1007\/978-3-642-39634-2_14","volume-title":"Interactive Theorem Proving","author":"G Gonthier","year":"2013","unstructured":"Gonthier, G., et al.: A machine-checked proof of the odd order theorem. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol. 7998, pp. 163\u2013179. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39634-2_14"},{"key":"6_CR30","unstructured":"Google: Google-Java-Format (2020). https:\/\/github.com\/google\/google-java-format . Accessed 23 Jan 2020"},{"key":"6_CR31","doi-asserted-by":"publisher","unstructured":"Hellendoorn, V.J., Devanbu, P.T., Alipour, M.A.: On the naturalness of proofs. In: International Symposium on the Foundations of Software Engineering, New Ideas and Emerging Results, pp. 724\u2013728. ACM, New York (2018). https:\/\/doi.org\/10.1145\/3236024.3264832","DOI":"10.1145\/3236024.3264832"},{"key":"6_CR32","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"354","DOI":"10.1007\/978-3-642-39320-4_28","volume-title":"Intelligent Computer Mathematics","author":"J Heras","year":"2013","unstructured":"Heras, J., Komendantskaya, E.: ML4PG in computer algebra verification. In: Carette, J., Aspinall, D., Lange, C., Sojka, P., Windsteiger, W. (eds.) CICM 2013. LNCS (LNAI), vol. 7961, pp. 354\u2013358. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39320-4_28"},{"key":"6_CR33","unstructured":"Heras, J., Komendantskaya, E.: Proof pattern search in Coq\/SSReflect. CoRR abs\/1402.0081 (2014). https:\/\/arxiv.org\/abs\/1402.0081"},{"issue":"1","key":"6_CR34","doi-asserted-by":"publisher","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. Math. Comput. Sci. 8(1), 99\u2013116 (2014). https:\/\/doi.org\/10.1007\/s11786-014-0173-1","journal-title":"Math. Comput. Sci."},{"key":"6_CR35","doi-asserted-by":"publisher","unstructured":"Hindle, A., Barr, E.T., Su, Z., Gabel, M., Devanbu, P.: On the naturalness of software. In: International Conference on Software Engineering, pp. 837\u2013847. IEEE Computer Society, Washington (2012). https:\/\/doi.org\/10.1109\/ICSE.2012.6227135","DOI":"10.1109\/ICSE.2012.6227135"},{"issue":"8","key":"6_CR36","doi-asserted-by":"publisher","first-page":"1735","DOI":"10.1162\/neco.1997.9.8.1735","volume":"9","author":"S Hochreiter","year":"1997","unstructured":"Hochreiter, S., Schmidhuber, J.: Long short-term memory. Neural Comput. 9(8), 1735\u20131780 (1997). https:\/\/doi.org\/10.1162\/neco.1997.9.8.1735","journal-title":"Neural Comput."},{"key":"6_CR37","unstructured":"HoTT authors: HoTT Conventions and Style Guide (2019). https:\/\/github.com\/HoTT\/HoTT\/blob\/V8.10\/STYLE.md . Accessed 23 Jan 2020"},{"key":"6_CR38","doi-asserted-by":"publisher","unstructured":"Hu, X., Li, G., Xia, X., Lo, D., Jin, Z.: Deep code comment generation. In: International Conference on Program Comprehension, pp. 200\u2013210. ACM, New York (2018). https:\/\/doi.org\/10.1145\/3196321.3196334","DOI":"10.1145\/3196321.3196334"},{"key":"6_CR39","unstructured":"Iris authors: Iris Style Guide (2019). https:\/\/gitlab.mpi-sws.org\/iris\/iris\/blob\/iris-3.2.0\/StyleGuide.md . Accessed 17 Apr 2020"},{"key":"6_CR40","unstructured":"Kingma, D.P., Ba, J.: Adam: a method for stochastic optimization. In: International Conference on Learning Representations (2015). https:\/\/arxiv.org\/abs\/1412.6980"},{"key":"6_CR41","doi-asserted-by":"publisher","unstructured":"Klein, G., Kim, Y., Deng, Y., Senellart, J., Rush, A.M.: OpenNMT: open-source toolkit for neural machine translation. In: Annual Meeting of the Association for Computational Linguistics, System Demonstrations, pp. 67\u201372. Association for Computational Linguistics, Stroudsburg (2017). https:\/\/doi.org\/10.18653\/v1\/P17-4012","DOI":"10.18653\/v1\/P17-4012"},{"key":"6_CR42","doi-asserted-by":"publisher","unstructured":"Komendantskaya, E., Heras, J., Grov, G.: Machine learning in Proof General: interfacing interfaces. In: Kaliszyk, C., L\u00fcth, C. (eds.) International Workshop on User Interfaces for Theorem Provers. EPTCS, vol. 118, pp. 15\u201341. Open Publishing Association, Sydney (2013). https:\/\/doi.org\/10.4204\/EPTCS.118.2","DOI":"10.4204\/EPTCS.118.2"},{"key":"6_CR43","doi-asserted-by":"publisher","unstructured":"LeClair, A., Jiang, S., McMillan, C.: A neural model for generating natural language summaries of program subroutines. In: International Conference on Software Engineering, pp. 795\u2013806. IEEE Computer Society, Washington (2019). https:\/\/doi.org\/10.1109\/ICSE.2019.00087","DOI":"10.1109\/ICSE.2019.00087"},{"issue":"7","key":"6_CR44","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1145\/1538788.1538814","volume":"52","author":"X Leroy","year":"2009","unstructured":"Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107\u2013115 (2009). https:\/\/doi.org\/10.1145\/1538788.1538814","journal-title":"Commun. ACM"},{"key":"6_CR45","doi-asserted-by":"publisher","unstructured":"Li, J., Galley, M., Brockett, C., Gao, J., Dolan, B.: A diversity-promoting objective function for neural conversation models. In: Conference of the North American Chapter of the Association for Computational Linguistics: Human Language Technologies, pp. 110\u2013119. Association for Computational Linguistics, Stroudsburg (2016). https:\/\/doi.org\/10.18653\/v1\/n16-1014","DOI":"10.18653\/v1\/n16-1014"},{"key":"6_CR46","doi-asserted-by":"crossref","unstructured":"Lin, C., Och, F.J.: ORANGE: a method for evaluating automatic evaluation metrics for machine translation. In: International Conference on Computational Linguistics, pp. 501\u2013507. Association for Computational Linguistics, Stroudsburg (2004)","DOI":"10.3115\/1220355.1220427"},{"key":"6_CR47","doi-asserted-by":"publisher","unstructured":"Liu, K., et al.: Learning to spot and refactor inconsistent method names. In: International Conference on Software Engineering, pp. 1\u201312. IEEE Computer Society, Washington (2019). https:\/\/doi.org\/10.1109\/ICSE.2019.00019","DOI":"10.1109\/ICSE.2019.00019"},{"key":"6_CR48","doi-asserted-by":"publisher","unstructured":"Luong, T., Pham, H., Manning, C.D.: Effective approaches to attention-based neural machine translation. In: Empirical Methods in Natural Language Processing, pp. 1412\u20131421. Association for Computational Linguistics, Stroudsburg (2015). https:\/\/doi.org\/10.18653\/v1\/d15-1166","DOI":"10.18653\/v1\/d15-1166"},{"key":"6_CR49","unstructured":"Mahboubi, A., Tassi, E.: Mathematical Components Book (2017). https:\/\/math-comp.github.io\/mcb\/ . Accessed 17 Apr 2020"},{"key":"6_CR50","unstructured":"Mathematical Components Team: Missing lemmas in Seq (2016). https:\/\/github.com\/math-comp\/math-comp\/pull\/41 . Accessed 18 Apr 2020"},{"issue":"4","key":"6_CR51","doi-asserted-by":"publisher","first-page":"184","DOI":"10.1145\/367177.367199","volume":"3","author":"J McCarthy","year":"1960","unstructured":"McCarthy, J.: Recursive functions of symbolic expressions and their computation by machine, part I. Commun. ACM 3(4), 184\u2013195 (1960). https:\/\/doi.org\/10.1145\/367177.367199","journal-title":"Commun. ACM"},{"issue":"11","key":"6_CR52","doi-asserted-by":"publisher","first-page":"861","DOI":"10.1145\/182.358437","volume":"26","author":"RJ Miara","year":"1983","unstructured":"Miara, R.J., Musselman, J.A., Navarro, J.A., Shneiderman, B.: Program indentation and comprehensibility. Commun. ACM 26(11), 861\u2013867 (1983). https:\/\/doi.org\/10.1145\/182.358437","journal-title":"Commun. ACM"},{"key":"6_CR53","unstructured":"de Moura, L., Avigad, J., Kong, S., Roux, C.: Elaboration in dependent type theory. CoRR abs\/1505.04324 (2015). https:\/\/arxiv.org\/abs\/1505.04324"},{"key":"6_CR54","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"378","DOI":"10.1007\/978-3-319-21401-6_26","volume-title":"Automated Deduction - CADE-25","author":"L de Moura","year":"2015","unstructured":"de Moura, L., Kong, S., Avigad, J., van Doorn, F., von Raumer, J.: The Lean theorem prover (system description). In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS (LNAI), vol. 9195, pp. 378\u2013388. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21401-6_26"},{"key":"6_CR55","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/978-3-030-23250-4_12","volume-title":"Intelligent Computer Mathematics","author":"D M\u00fcller","year":"2019","unstructured":"M\u00fcller, D., Rabe, F., Sacerdoti Coen, C.: The Coq library as a theory graph. In: Kaliszyk, C., Brady, E., Kohlhase, A., Sacerdoti Coen, C. (eds.) CICM 2019. LNCS (LNAI), vol. 11617, pp. 171\u2013186. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-23250-4_12"},{"key":"6_CR56","unstructured":"Nanevski, A., Ley-Wild, R., Sergey, I., Delbianco, G., Trunov, A.: The PCM library (2020). https:\/\/github.com\/imdea-software\/fcsl-pcm . Accessed 24 Jan 2020"},{"key":"6_CR57","unstructured":"Nie, P., Palmskog, K., Li, J.J., Gligoric, M.: Deep generation of Coq lemma names using elaborated terms. CoRR abs\/2004.07761 (2020). https:\/\/arxiv.org\/abs\/2004.07761"},{"key":"6_CR58","unstructured":"OCaml Labs: PPX (2017). http:\/\/ocamllabs.io\/doc\/ppx.html . Accessed 23 Jan 2020"},{"key":"6_CR59","doi-asserted-by":"publisher","unstructured":"Ogura, N., Matsumoto, S., Hata, H., Kusumoto, S.: Bring your own coding style. In: International Conference on Software Analysis, Evolution and Reengineering, pp. 527\u2013531. IEEE Computer Society, Washington (2018). https:\/\/doi.org\/10.1109\/SANER.2018.8330253","DOI":"10.1109\/SANER.2018.8330253"},{"key":"6_CR60","doi-asserted-by":"crossref","unstructured":"Papineni, K., Roukos, S., Ward, T., Zhu, W.: BLEU: a method for automatic evaluation of machine translation. In: Annual Meeting of the Association for Computational Linguistics, pp. 311\u2013318. Association for Computational Linguistics, Stroudsburg (2002)","DOI":"10.3115\/1073083.1073135"},{"key":"6_CR61","unstructured":"Paszke, A., et al.: Automatic differentiation in PyTorch. In: Autodiff Workshop (2017). https:\/\/openreview.net\/forum?id=BJJsrmfCZ"},{"key":"6_CR62","doi-asserted-by":"publisher","unstructured":"Rahman, M., Palani, D., Rigby, P.C.: Natural software revisited. In: International Conference on Software Engineering, pp. 37\u201348. IEEE Computer Society, Washington (2019). https:\/\/doi.org\/10.1109\/ICSE.2019.00022","DOI":"10.1109\/ICSE.2019.00022"},{"key":"6_CR63","doi-asserted-by":"publisher","unstructured":"Raychev, V., Vechev, M., Krause, A.: Predicting program properties from \u201cbig code\u201d. In: Symposium on Principles of Programming Languages, pp. 111\u2013124. ACM, New York (2015). https:\/\/doi.org\/10.1145\/2676726.2677009","DOI":"10.1145\/2676726.2677009"},{"key":"6_CR64","doi-asserted-by":"publisher","unstructured":"See, A., Liu, P.J., Manning, C.D.: Get to the point: summarization with pointer-generator networks. In: Annual Meeting of the Association for Computational Linguistics, pp. 1073\u20131083. Association for Computational Linguistics, Stroudsburg (2017). https:\/\/doi.org\/10.18653\/v1\/P17-1099","DOI":"10.18653\/v1\/P17-1099"},{"key":"6_CR65","doi-asserted-by":"crossref","unstructured":"Serban, I.V., Sordoni, A., Bengio, Y., Courville, A., Pineau, J.: Building end-to-end dialogue systems using generative hierarchical neural network models. In: AAAI Conference on Artificial Intelligence, pp. 3776\u20133783. AAAI Press, Palo Alto (2016)","DOI":"10.1609\/aaai.v30i1.9883"},{"key":"6_CR66","doi-asserted-by":"publisher","unstructured":"Sergey, I., Nanevski, A., Banerjee, A.: Mechanized verification of fine-grained concurrent programs. In: Conference on Programming Language Design and Implementation, pp. 77\u201387. ACM, New York (2015). https:\/\/doi.org\/10.1145\/2737924.2737964","DOI":"10.1145\/2737924.2737964"},{"issue":"24","key":"6_CR67","doi-asserted-by":"publisher","first-page":"557","DOI":"10.1177\/154193127602002401","volume":"20","author":"B Shneiderman","year":"1976","unstructured":"Shneiderman, B., McKay, D.: Experimental investigations of computer program debugging and modification. Hum. Factors Soc. Ann. Meet. 20(24), 557\u2013563 (1976). https:\/\/doi.org\/10.1177\/154193127602002401","journal-title":"Hum. Factors Soc. Ann. Meet."},{"key":"6_CR68","unstructured":"Sutskever, I., Vinyals, O., Le, Q.V.: Sequence to sequence learning with neural networks. In: Advances in Neural Information Processing Systems 27, pp. 3104\u20133112. MIT Press, Cambridge (2014)"},{"key":"6_CR69","doi-asserted-by":"publisher","unstructured":"Suzuki, J., Nagata, M.: Cutting-off redundant repeating generations for neural abstractive summarization. In: Conference of the European Chapter of the Association for Computational Linguistics, pp. 291\u2013297. Association for Computational Linguistics, Stroudsburg (2017). https:\/\/doi.org\/10.18653\/v1\/e17-2047","DOI":"10.18653\/v1\/e17-2047"},{"key":"6_CR70","doi-asserted-by":"publisher","unstructured":"Unanue, I.J., Borzeshi, E.Z., Piccardi, M.: A shared attention mechanism for interpretation of neural automatic post-editing systems. In: Workshop on Neural Machine Translation and Generation, pp. 11\u201317. Association for Computational Linguistics, Stroudsburg (2018). https:\/\/doi.org\/10.18653\/v1\/w18-2702","DOI":"10.18653\/v1\/w18-2702"},{"issue":"31","key":"6_CR71","first-page":"137","volume":"18","author":"F Wiedijk","year":"2009","unstructured":"Wiedijk, F.: Statistics on digital libraries of mathematics. Stud. Logic Gramm. Rhetor. 18(31), 137\u2013151 (2009)","journal-title":"Stud. Logic Gramm. Rhetor."},{"issue":"2","key":"6_CR72","doi-asserted-by":"publisher","first-page":"270","DOI":"10.1162\/neco.1989.1.2.270","volume":"1","author":"RJ Williams","year":"1989","unstructured":"Williams, R.J., Zipser, D.: A learning algorithm for continually running fully recurrent neural networks. Neural Comput. 1(2), 270\u2013280 (1989). https:\/\/doi.org\/10.1162\/neco.1989.1.2.270","journal-title":"Neural Comput."},{"key":"6_CR73","doi-asserted-by":"publisher","unstructured":"Woos, D., Wilcox, J.R., Anton, S., Tatlock, Z., Ernst, M.D., Anderson, T.: Planning for change in a formal verification of the Raft consensus protocol. In: Certified Programs and Proofs, pp. 154\u2013165. ACM, New York (2016). https:\/\/doi.org\/10.1145\/2854065.2854081","DOI":"10.1145\/2854065.2854081"},{"key":"6_CR74","doi-asserted-by":"publisher","unstructured":"Xu, S., Zhang, S., Wang, W., Cao, X., Guo, C., Xu, J.: Method name suggestion with hierarchical attention networks. In: Workshop on Partial Evaluation and Program Manipulation, pp. 10\u201321. ACM, New York (2019). https:\/\/doi.org\/10.1145\/3294032.3294079","DOI":"10.1145\/3294032.3294079"},{"key":"6_CR75","doi-asserted-by":"publisher","unstructured":"Zhang, S., Zheng, D., Hu, X., Yang, M.: Bidirectional long short-term memory networks for relation classification. In: Pacific Asia Conference on Language, Information and Computation, pp. 207\u2013212. Association for Computational Linguistics, Stroudsburg (2015). https:\/\/doi.org\/10.18653\/v1\/p16-2034","DOI":"10.18653\/v1\/p16-2034"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-51054-1_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,10,30]],"date-time":"2022-10-30T21:38:26Z","timestamp":1667165906000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-51054-1_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030510534","9783030510541"],"references-count":75,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-51054-1_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"24 June 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"IJCAR","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Joint Conference on Automated Reasoning","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Paris","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"1 July 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"4 July 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"ijcar2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/ijcar2020.org\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"150","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"46","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"5","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"31% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3.03","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"7.38","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"No","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"11 system descriptions are also included. The conference was held virtually due to the COVID-19 pandemic.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}