{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,6]],"date-time":"2026-06-06T03:49:18Z","timestamp":1780717758330,"version":"3.54.1"},"publisher-location":"New York, NY, USA","reference-count":46,"publisher":"ACM","license":[{"start":{"date-parts":[[2020,6,15]],"date-time":"2020-06-15T00:00:00Z","timestamp":1592179200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2020,6,15]]},"DOI":"10.1145\/3394450.3397466","type":"proceedings-article","created":{"date-parts":[[2020,6,1]],"date-time":"2020-06-01T22:03:54Z","timestamp":1591049034000},"page":"1-10","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":31,"title":["Generating correctness proofs with neural networks"],"prefix":"10.1145","author":[{"given":"Alex","family":"Sanchez-Stern","sequence":"first","affiliation":[{"name":"University of California at San Diego, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Yousef","family":"Alhessi","sequence":"additional","affiliation":[{"name":"University of California at San Diego, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Lawrence","family":"Saul","sequence":"additional","affiliation":[{"name":"University of California at San Diego, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Sorin","family":"Lerner","sequence":"additional","affiliation":[{"name":"University of California at San Diego, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2020,6,15]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"Alexander A. Alemi Fran\u00e7ois Chollet Geoffrey Irving Christian Szegedy and Josef Urban. 2016. DeepMath - Deep Sequence Models for Premise Selection. CoRR abs\/1606.04442 (2016). arXiv: 1606.04442 http:\/\/arxiv.org\/abs\/1606.04442  Alexander A. Alemi Fran\u00e7ois Chollet Geoffrey Irving Christian Szegedy and Josef Urban. 2016. DeepMath - Deep Sequence Models for Premise Selection. CoRR abs\/1606.04442 (2016). arXiv: 1606.04442 http:\/\/arxiv.org\/abs\/1606.04442"},{"key":"e_1_3_2_1_2_1","unstructured":"Miltiadis Allamanis Earl T. Barr Premkumar T. Devanbu and Charles A. Sutton. 2017. A Survey of Machine Learning for Big Code and Naturalness. CoRR abs\/1709.06182 (2017). arXiv: 1709.06182 http:\/\/arxiv.org\/abs\/1709.06182  Miltiadis Allamanis Earl T. Barr Premkumar T. Devanbu and Charles A. Sutton. 2017. A Survey of Machine Learning for Big Code and Naturalness. CoRR abs\/1709.06182 (2017). arXiv: 1709.06182 http:\/\/arxiv.org\/abs\/1709.06182"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/2701415"},{"key":"e_1_3_2_1_4_1","volume-title":"Proceedings of the 32nd International Conference on Neural Information Processing Systems (NIPS\u201918)","author":"Balunoviundefined Mislav","year":"2018"},{"key":"e_1_3_2_1_5_1","unstructured":"Kshitij Bansal Sarah M. Loos Markus N. Rabe Christian Szegedy and Stewart Wilcox. 2019.  Kshitij Bansal Sarah M. Loos Markus N. Rabe Christian Szegedy and Stewart Wilcox. 2019."},{"key":"e_1_3_2_1_6_1","unstructured":"HOList: An Environment for Machine Learning of Higher-Order Theorem Proving (extended version). CoRR abs\/1904.03241 (2019). arXiv: 1904.03241 http:\/\/arxiv.org\/abs\/1904.03241  HOList: An Environment for Machine Learning of Higher-Order Theorem Proving (extended version). CoRR abs\/1904.03241 (2019). arXiv: 1904.03241 http:\/\/arxiv.org\/abs\/1904.03241"},{"key":"e_1_3_2_1_7_1","unstructured":"Clark Barrett Christopher L. Conway Morgan Deters Liana Hadarean Dejan Jovanovi\u0107 Tim King Andrew Reynolds and Cesare Tinelli. 2011.  Clark Barrett Christopher L. Conway Morgan Deters Liana Hadarean Dejan Jovanovi\u0107 Tim King Andrew Reynolds and Cesare Tinelli. 2011."},{"key":"e_1_3_2_1_8_1","volume-title":"Proceedings of the 23rd International Conference on Computer Aided Verification (CAV\u201911)","year":"2032"},{"key":"e_1_3_2_1_9_1","volume-title":"Proceedings of The 33rd International Conference on Machine Learning (Proceedings of Machine Learning Research), Maria Florina Balcan and Kilian Q. Weinberger (Eds.)","volume":"48","author":"Bielik Pavol","year":"2016"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3132747.3132776"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"crossref","unstructured":"Adam Chlipala. 2013. Certified Programming with Dependent Types: A Pragmatic Introduction to the Coq Proof Assistant. The MIT Press.  Adam Chlipala. 2013. Certified Programming with Dependent Types: A Pragmatic Introduction to the Coq Proof Assistant. The MIT Press.","DOI":"10.7551\/mitpress\/9153.001.0001"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-018-9458-4"},{"key":"e_1_3_2_1_13_1","unstructured":"Hoa Khanh Dam Truyen Tran and Trang Pham. 2016. A deep language model for software code. CoRR abs\/1608.02715 (2016). arXiv: 1608.02715 http:\/\/arxiv.org\/abs\/1608.02715  Hoa Khanh Dam Truyen Tran and Trang Pham. 2016. A deep language model for software code. CoRR abs\/1608.02715 (2016). arXiv: 1608.02715 http:\/\/arxiv.org\/abs\/1608.02715"},{"key":"e_1_3_2_1_14_1","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"de Moura Leonardo"},{"key":"e_1_3_2_1_16_1","unstructured":"Jonathan Frankle Peter-Michael Osera David Walker and S Zdancewic. 2016.  Jonathan Frankle Peter-Michael Osera David Walker and S Zdancewic. 2016."},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2914770.2837629"},{"key":"e_1_3_2_1_18_1","unstructured":"Pranav Garg Daniel Neider P. Madhusudan and Dan Roth. 2016.  Pranav Garg Daniel Neider P. Madhusudan and Dan Roth. 2016."},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2914770.2837664"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.29007\/ntlb"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"crossref","unstructured":"Sumit Gulwani. 2010. Dimensions in Program Synthesis. In PPDP \u201910 Hagenberg Austria (ppdp \u201910 hagenberg austria ed.). https:\/\/www.microsoft.com\/en-us\/research\/publication\/dimensionsprogram-synthesis\/  Sumit Gulwani. 2010. Dimensions in Program Synthesis. In PPDP \u201910 Hagenberg Austria (ppdp \u201910 hagenberg austria ed.). https:\/\/www.microsoft.com\/en-us\/research\/publication\/dimensionsprogram-synthesis\/","DOI":"10.1145\/1836089.1836091"},{"key":"e_1_3_2_1_22_1","first-page":"12","article-title":"Complete Completion using Types and Weights","volume":"2013","author":"Gvero Tihomir","year":"2013","journal-title":"PLDI"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.152.5"},{"key":"e_1_3_2_1_24_1","unstructured":"Daniel Huang Prafulla Dhariwal Dawn Song and Ilya Sutskever. 2018.  Daniel Huang Prafulla Dhariwal Dawn Song and Ilya Sutskever. 2018."},{"key":"e_1_3_2_1_25_1","unstructured":"GamePad: A Learning Environment for Theorem Proving. CoRR abs\/1806.00608 (2018).  GamePad: A Learning Environment for Theorem Proving. CoRR abs\/1806.00608 (2018)."},{"key":"e_1_3_2_1_26_1","unstructured":"arXiv: 1806.00608 http:\/\/arxiv.org\/abs\/1806.00608  arXiv: 1806.00608 http:\/\/arxiv.org\/abs\/1806.00608"},{"key":"e_1_3_2_1_27_1","unstructured":"Cezary Kaliszyk Fran\u00e7ois Chollet and Christian Szegedy. 2017. HolStep: A Machine Learning Dataset for Higher-order Logic Theorem Proving. CoRR abs\/1703.00426 (2017). arXiv: 1703.00426 http:\/\/arxiv.org\/abs\/1703.00426  Cezary Kaliszyk Fran\u00e7ois Chollet and Christian Szegedy. 2017. HolStep: A Machine Learning Dataset for Higher-order Logic Theorem Proving. CoRR abs\/1703.00426 (2017). arXiv: 1703.00426 http:\/\/arxiv.org\/abs\/1703.00426"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629596"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.118.2"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33266-1_53"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_1"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3106237.3106253"},{"key":"e_1_3_2_1_34_1","unstructured":"Sarah M. Loos Geoffrey Irving Christian Szegedy and Cezary Kaliszyk. 2017. Deep Network Guided Proof Search. CoRR abs\/1701.06972 (2017).  Sarah M. Loos Geoffrey Irving Christian Szegedy and Cezary Kaliszyk. 2017. Deep Network Guided Proof Search. CoRR abs\/1701.06972 (2017)."},{"key":"e_1_3_2_1_35_1","unstructured":"arXiv: 1701.06972 http:\/\/arxiv.org\/abs\/1701.06972  arXiv: 1701.06972 http:\/\/arxiv.org\/abs\/1701.06972"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706329"},{"key":"e_1_3_2_1_37_1","volume-title":"June 15, 2020","author":"Mou Lili","year":"2014"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/2813885.2738007"},{"key":"e_1_3_2_1_39_1","unstructured":"Aditya Paliwal Sarah M. Loos Markus N. Rabe Kshitij Bansal and Christian Szegedy. 2019. Graph Representations for Higher-Order Logic and Theorem Proving. CoRR abs\/1905.10006 (2019). arXiv: 1905.10006 http:\/\/arxiv.org\/abs\/1905.10006  Aditya Paliwal Sarah M. Loos Markus N. Rabe Kshitij Bansal and Christian Szegedy. 2019. Graph Representations for Higher-Order Logic and Theorem Proving. CoRR abs\/1905.10006 (2019). arXiv: 1905.10006 http:\/\/arxiv.org\/abs\/1905.10006"},{"key":"e_1_3_2_1_40_1","unstructured":"Lawrence C. Paulson. 1993. Natural Deduction as Higher-Order Resolution. CoRR cs.LO\/9301104 (1993). http:\/\/arxiv.org\/abs\/cs.LO\/9301104  Lawrence C. Paulson. 1993. Natural Deduction as Higher-Order Resolution. CoRR cs.LO\/9301104 (1993). http:\/\/arxiv.org\/abs\/cs.LO\/9301104"},{"key":"e_1_3_2_1_41_1","volume-title":"System Description: E 1.8. In Proc. of the 19th LPAR, Stellenbosch (LNCS)","author":"Schulz Stephan","year":"2013"},{"key":"e_1_3_2_1_42_1","unstructured":"Taro Sekiyama Akifumi Imanishi and Kohei Suenaga. 2017. Towards Proof Synthesis Guided by Neural Machine Translation for Intuitionistic Propositional Logic. CoRR abs\/1706.06462 (2017). arXiv: 1706.06462 http:\/\/arxiv.org\/abs\/1706.06462  Taro Sekiyama Akifumi Imanishi and Kohei Suenaga. 2017. Towards Proof Synthesis Guided by Neural Machine Translation for Intuitionistic Propositional Logic. CoRR abs\/1706.06462 (2017). arXiv: 1706.06462 http:\/\/arxiv.org\/abs\/1706.06462"},{"key":"e_1_3_2_1_43_1","first-page":"1","article-title":"GNU Parallel - The Command-Line Power Tool. ;login","volume":"36","author":"Tange O.","year":"2011","journal-title":"The USENIX Magazine"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737958"},{"key":"e_1_3_2_1_45_1","unstructured":"Kaiyu Yang and Jia Deng. 2019. Learning to Prove Theorems via Interacting with Proof Assistants. CoRR abs\/1905.09381 (2019).  Kaiyu Yang and Jia Deng. 2019. Learning to Prove Theorems via Interacting with Proof Assistants. CoRR abs\/1905.09381 (2019)."},{"key":"e_1_3_2_1_46_1","unstructured":"arXiv: 1905.09381 http:\/\/arxiv.org\/abs\/1905.09381  arXiv: 1905.09381 http:\/\/arxiv.org\/abs\/1905.09381"},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"crossref","unstructured":"Xuejun Yang Yang Chen Eric Eide and John Regehr. 2011. Finding and Understanding Bugs in C Compilers. PLDI (2011).  Xuejun Yang Yang Chen Eric Eide and John Regehr. 2011. Finding and Understanding Bugs in C Compilers. PLDI (2011).","DOI":"10.1145\/1993498.1993532"}],"event":{"name":"PLDI '20: 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation","location":"London UK","acronym":"PLDI '20","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"]},"container-title":["Proceedings of the 4th ACM SIGPLAN International Workshop on Machine Learning and Programming Languages"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3394450.3397466","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3394450.3397466","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:41:37Z","timestamp":1750200097000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3394450.3397466"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,6,15]]},"references-count":46,"alternative-id":["10.1145\/3394450.3397466","10.1145\/3394450"],"URL":"https:\/\/doi.org\/10.1145\/3394450.3397466","relation":{},"subject":[],"published":{"date-parts":[[2020,6,15]]},"assertion":[{"value":"2020-06-15","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}