{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,21]],"date-time":"2026-03-21T02:43:16Z","timestamp":1774060996131,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":15,"publisher":"ACM","license":[{"start":{"date-parts":[[2019,9,23]],"date-time":"2019-09-23T00:00:00Z","timestamp":1569196800000},"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":[[2019,9,23]]},"DOI":"10.1145\/3355378.3355379","type":"proceedings-article","created":{"date-parts":[[2019,9,5]],"date-time":"2019-09-05T12:16:25Z","timestamp":1567685785000},"page":"46-53","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":5,"title":["Structure verification of deep neural networks at compilation time using dependent types"],"prefix":"10.1145","author":[{"given":"Leonardo","family":"Pi\u00f1eyro","sequence":"first","affiliation":[{"name":"Instituto de Computaci\u00f3n, Universidad de la Rep\u00fablica, Montevideo, Uruguay"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alberto","family":"Pardo","sequence":"additional","affiliation":[{"name":"Instituto de Computaci\u00f3n, Universidad de la Rep\u00fablica, Montevideo, Uruguay"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marcos","family":"Viera","sequence":"additional","affiliation":[{"name":"Instituto de Computaci\u00f3n, Universidad de la Rep\u00fablica, Montevideo, Uruguay"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2019,9,23]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"Tensorflow: A system for large-scale machine learning. In 12th {USENIX} Symposium on Operating Systems Design and Implementation ({OSDI} 16). 265--283.","author":"Abadi Mart\u00edn","year":"2016","unstructured":"Mart\u00edn Abadi , Paul Barham , Jianmin Chen , Zhifeng Chen , Andy Davis , Jeffrey Dean , Matthieu Devin , Sanjay Ghemawat , Geoffrey Irving , Michael Isard , 2016 . Tensorflow: A system for large-scale machine learning. In 12th {USENIX} Symposium on Operating Systems Design and Implementation ({OSDI} 16). 265--283. Mart\u00edn Abadi, Paul Barham, Jianmin Chen, Zhifeng Chen, Andy Davis, Jeffrey Dean, Matthieu Devin, Sanjay Ghemawat, Geoffrey Irving, Michael Isard, et al. 2016. Tensorflow: A system for large-scale machine learning. In 12th {USENIX} Symposium on Operating Systems Design and Implementation ({OSDI} 16). 265--283."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10994-010-5188-5"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3136000.3136001"},{"key":"e_1_3_2_1_4_1","unstructured":"Fran\u00e7ois Chollet. 2015. keras. https:\/\/github.com\/fchollet\/keras.  Fran\u00e7ois Chollet. 2015. keras. https:\/\/github.com\/fchollet\/keras."},{"key":"e_1_3_2_1_5_1","volume-title":"Twenty-Second International Joint Conference on Artificial Intelligence.","author":"Ciresan Dan Claudiu","year":"2011","unstructured":"Dan Claudiu Ciresan , Ueli Meier , Jonathan Masci , Luca Maria Gambardella , and J\u00fcrgen Schmidhuber . 2011 . Flexible, high performance convolutional neural networks for image classification . In Twenty-Second International Joint Conference on Artificial Intelligence. Dan Claudiu Ciresan, Ueli Meier, Jonathan Masci, Luca Maria Gambardella, and J\u00fcrgen Schmidhuber. 2011. Flexible, high performance convolutional neural networks for image classification. In Twenty-Second International Joint Conference on Artificial Intelligence."},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1109\/MSP.2012.2211477"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2430532.2364522"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1109\/CVPR.2016.90"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63387-9_1"},{"key":"e_1_3_2_1_10_1","volume-title":"Deep learning. nature 521, 7553","author":"LeCun Yann","year":"2015","unstructured":"Yann LeCun , Yoshua Bengio , and Geoffrey Hinton . 2015. Deep learning. nature 521, 7553 ( 2015 ), 436. Yann LeCun, Yoshua Bengio, and Geoffrey Hinton. 2015. Deep learning. nature 521, 7553 (2015), 436."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796802004355"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1109\/SURV.2008.080406"},{"key":"e_1_3_2_1_13_1","volume-title":"Automatic Differentiation in PyTorch. In NIPS Autodiff Workshop.","author":"Paszke Adam","year":"2017","unstructured":"Adam Paszke , Sam Gross , Soumith Chintala , Gregory Chanan , Edward Yang , Zachary DeVito , Zeming Lin , Alban Desmaison , Luca Antiga , and Adam Lerer . 2017 . Automatic Differentiation in PyTorch. In NIPS Autodiff Workshop. Adam Paszke, Sam Gross, Soumith Chintala, Gregory Chanan, Edward Yang, Zachary DeVito, Zeming Lin, Alban Desmaison, Luca Antiga, and Adam Lerer. 2017. Automatic Differentiation in PyTorch. In NIPS Autodiff Workshop."},{"key":"e_1_3_2_1_14_1","volume-title":"Modeling of languages for tensor manipulation. CoRR abs\/1801.08771","author":"Rink Norman A.","year":"2018","unstructured":"Norman A. Rink . 2018. Modeling of languages for tensor manipulation. CoRR abs\/1801.08771 ( 2018 ). arXiv:1801.08771 http:\/\/arxiv.org\/abs\/1801.08771 Norman A. Rink. 2018. Modeling of languages for tensor manipulation. CoRR abs\/1801.08771 (2018). arXiv:1801.08771 http:\/\/arxiv.org\/abs\/1801.08771"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103786.2103795"}],"event":{"name":"SBLP 2019: XXIII Brazilian Symposium on Programming Languages","location":"Salvador Brazil","acronym":"SBLP 2019","sponsor":["SBC Sociedade Brasileira de Computa\u00e7\u00e3o"]},"container-title":["Proceedings of the XXIII Brazilian Symposium on Programming Languages"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3355378.3355379","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3355378.3355379","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:23:33Z","timestamp":1750202613000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3355378.3355379"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,9,23]]},"references-count":15,"alternative-id":["10.1145\/3355378.3355379","10.1145\/3355378"],"URL":"https:\/\/doi.org\/10.1145\/3355378.3355379","relation":{},"subject":[],"published":{"date-parts":[[2019,9,23]]},"assertion":[{"value":"2019-09-23","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}