{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,10,30]],"date-time":"2024-10-30T20:13:03Z","timestamp":1730319183751,"version":"3.28.0"},"publisher-location":"New York, NY, USA","reference-count":21,"publisher":"ACM","license":[{"start":{"date-parts":[[2017,6,18]],"date-time":"2017-06-18T00:00:00Z","timestamp":1497744000000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2017,6,18]]},"DOI":"10.1145\/3088525.3088673","type":"proceedings-article","created":{"date-parts":[[2017,6,9]],"date-time":"2017-06-09T17:40:22Z","timestamp":1497030022000},"page":"43-50","update-policy":"http:\/\/dx.doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["Verified perceptron convergence theorem"],"prefix":"10.1145","author":[{"given":"Charlie","family":"Murphy","sequence":"first","affiliation":[{"name":"Princeton University, USA"}]},{"given":"Patrick","family":"Gray","sequence":"additional","affiliation":[{"name":"Ohio University, USA"}]},{"given":"Gordon","family":"Stewart","sequence":"additional","affiliation":[{"name":"Ohio University, USA"}]}],"member":"320","published-online":{"date-parts":[[2017,6,18]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1051\/ita:2004015"},{"key":"e_1_3_2_1_2_1","first-page":"2","article-title":"The Irises of the Gasp\u00e9 Peninsula","volume":"59","author":"Anderson Edgar","year":"1935","unstructured":"Edgar Anderson . The Irises of the Gasp\u00e9 Peninsula . Bulletin of the American Iris Society , 59 : 2 \u2013 5 , 1935 . Edgar Anderson. The Irises of the Gasp\u00e9 Peninsula. Bulletin of the American Iris Society, 59:2\u20135, 1935.","journal-title":"Bulletin of the American Iris Society"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676724.2693172"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1103\/RevModPhys.34.123"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1109\/ARITH.2011.40"},{"volume-title":"Aut. Deduction in Geom.","year":"2012","author":"Brun Christophe","key":"e_1_3_2_1_7_1","unstructured":"Christophe Brun , Jean-Fran\u00e7ois Dufourd , and Nicolas Magaud . Formal Proof in Coq and Derivation of an Imperative Program to Compute Convex Hulls . In Aut. Deduction in Geom. 2012 . Christophe Brun, Jean-Fran\u00e7ois Dufourd, and Nicolas Magaud. Formal Proof in Coq and Derivation of an Imperative Program to Compute Convex Hulls. In Aut. Deduction in Geom. 2012."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1109\/78.175745"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/1133981.1134029"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1162\/jmlr.2003.3.4-5.951"},{"issue":"2","key":"e_1_3_2_1_11_1","first-page":"179","article-title":"A course in machine learning. http:\/\/ciml.info\/, 2017. Accessed: 2017-03-22","volume":"7","author":"Daum\u00e9 Hal","year":"1936","unstructured":"Hal Daum\u00e9 , III . A course in machine learning. http:\/\/ciml.info\/, 2017. Accessed: 2017-03-22 . Ronald A Fisher. The Use of Multiple Measurements in Taxonomic Problems. Annals of Eugenics , 7 ( 2 ): 179 \u2013 188 , 1936 . Hal Daum\u00e9, III. A course in machine learning. http:\/\/ciml.info\/, 2017. Accessed: 2017-03-22. Ronald A Fisher. The Use of Multiple Measurements in Taxonomic Problems. Annals of Eugenics, 7(2):179\u2013188, 1936.","journal-title":"Ronald A Fisher. The Use of Multiple Measurements in Taxonomic Problems. Annals of Eugenics"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/11814771_36"},{"volume-title":"Deep learning with limited numerical precision. CoRR, abs\/1502.02551, 392","year":"2015","author":"Gupta Suyog","key":"e_1_3_2_1_13_1","unstructured":"Suyog Gupta , Ankur Agrawal , Kailash Gopalakrishnan , and Pritish Narayanan . Deep learning with limited numerical precision. CoRR, abs\/1502.02551, 392 , 2015 . Suyog Gupta, Ankur Agrawal, Kailash Gopalakrishnan, and Pritish Narayanan. Deep learning with limited numerical precision. CoRR, abs\/1502.02551, 392, 2015."},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-45221-5_27"},{"volume-title":"Machine Learning in Proof General: Interfacing Interfaces. arXiv preprint arXiv:1212.3618","year":"2012","author":"Komendantskaya Ekaterina","key":"e_1_3_2_1_15_1","unstructured":"Ekaterina Komendantskaya , J\u00f3nathan Heras , and Gudmund Grov . Machine Learning in Proof General: Interfacing Interfaces. arXiv preprint arXiv:1212.3618 , 2012 . Ekaterina Komendantskaya, J\u00f3nathan Heras, and Gudmund Grov. Machine Learning in Proof General: Interfacing Interfaces. arXiv preprint arXiv:1212.3618, 2012."},{"volume-title":"UCI Machine Learning Repository","year":"2013","author":"Lichman M.","key":"e_1_3_2_1_16_1","unstructured":"M. Lichman . UCI Machine Learning Repository , 2013 . M. Lichman. UCI Machine Learning Repository, 2013."},{"volume-title":"Towards a Practical Programming Language Based on Dependent Type Theory","year":"2007","author":"Norell Ulf","key":"e_1_3_2_1_17_1","unstructured":"Ulf Norell . Towards a Practical Programming Language Based on Dependent Type Theory , 2007 . Ulf Norell. Towards a Practical Programming Language Based on Dependent Type Theory, 2007."},{"volume-title":"Proceedings of the Fourth London Symposium on Information Theory","year":"1961","author":"Papert Seymour","key":"e_1_3_2_1_18_1","unstructured":"Seymour Papert . Some mathematical models of learning . In Proceedings of the Fourth London Symposium on Information Theory , 1961 . Seymour Papert. Some mathematical models of learning. In Proceedings of the Fourth London Symposium on Information Theory, 1961."},{"first-page":"361","volume-title":"International Conference on Theorem Proving in Higher Order Logics","author":"Pichardie David","key":"e_1_3_2_1_19_1","unstructured":"David Pichardie and Yves Bertot . Formalizing convex hull algorithms . In International Conference on Theorem Proving in Higher Order Logics , pages 346\u2013 361 . Springer, 2001. David Pichardie and Yves Bertot. Formalizing convex hull algorithms. In International Conference on Theorem Proving in Higher Order Logics, pages 346\u2013361. Springer, 2001."},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2854065.2854066"},{"volume-title":"Principles of Neurodynamics","year":"1962","author":"Rosenblatt Frank","key":"e_1_3_2_1_22_1","unstructured":"Frank Rosenblatt . Principles of Neurodynamics ; Perceptrons and the Theory of Brain Mechanisms. Spartan Books , 1962 . Frank Rosenblatt. Principles of Neurodynamics; Perceptrons and the Theory of Brain Mechanisms. Spartan Books, 1962."},{"volume-title":"The Coq Proof Assistant. https:\/\/coq. inria.fr\/","year":"2016","author":"Development Team The Coq","key":"e_1_3_2_1_23_1","unstructured":"The Coq Development Team . The Coq Proof Assistant. https:\/\/coq. inria.fr\/ , 2016 . {Online; accessed 2-19-2016}. Dimitrios Vytiniotis, Thierry Coquand , and David Wahlstedt. Stop When You Are Almost-Full. In ITP. 2012. The Coq Development Team. The Coq Proof Assistant. https:\/\/coq. inria.fr\/, 2016. {Online; accessed 2-19-2016}. Dimitrios Vytiniotis, Thierry Coquand, and David Wahlstedt. Stop When You Are Almost-Full. In ITP. 2012."}],"event":{"name":"PLDI '17: ACM SIGPLAN Conference on Programming Language Design and Implementation","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"],"location":"Barcelona Spain","acronym":"PLDI '17"},"container-title":["Proceedings of the 1st ACM SIGPLAN International Workshop on Machine Learning and Programming Languages"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3088525.3088673","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,7]],"date-time":"2023-01-07T12:15:31Z","timestamp":1673093731000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3088525.3088673"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,6,18]]},"references-count":21,"alternative-id":["10.1145\/3088525.3088673","10.1145\/3088525"],"URL":"http:\/\/dx.doi.org\/10.1145\/3088525.3088673","relation":{},"subject":[],"published":{"date-parts":[[2017,6,18]]},"assertion":[{"value":"2017-06-18","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}