{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T16:25:53Z","timestamp":1743006353595,"version":"3.40.3"},"publisher-location":"Cham","reference-count":34,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031300431"},{"type":"electronic","value":"9783031300448"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,4,17]],"date-time":"2023-04-17T00:00:00Z","timestamp":1681689600000},"content-version":"vor","delay-in-days":106,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Tensor shape mismatch is a common source of bugs in deep learning programs. We propose a new type-based approach to detect tensor shape mismatches. One of the main features of our approach is the best-effort shape inference. As the tensor shape inference problem is undecidable in general, we allow static type\/shape inference to be performed only in a best-effort manner. If the static inference cannot guarantee the absence of the shape inconsistencies, dynamic checks are inserted into the program. Another main feature is gradual typing, where users can improve the precision of the inference by adding appropriate type annotations to the program. We formalize our approach and prove that it satisfies the criteria of gradual typing proposed by Siek et al. in 2015. We have implemented a prototype shape checking tool based on our approach and evaluated its effectiveness by applying it to some deep neural network programs.<\/jats:p>","DOI":"10.1007\/978-3-031-30044-8_8","type":"book-chapter","created":{"date-parts":[[2023,4,16]],"date-time":"2023-04-16T20:28:25Z","timestamp":1681676905000},"page":"197-224","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Gradual Tensor Shape Checking"],"prefix":"10.1007","author":[{"given":"Momoko","family":"Hattori","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0537-0604","authenticated-orcid":false,"given":"Naoki","family":"Kobayashi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8679-2747","authenticated-orcid":false,"given":"Ryosuke","family":"Sato","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2023,4,17]]},"reference":[{"key":"8_CR1","unstructured":"Abadi, M., Agarwal, A., Barham, P., Brevdo, E., Chen, Z., Citro, C., Corrado, G.S., Davis, A., Dean, J., Devin, M., et\u00a0al.: Tensorflow: Large-scale machine learning on heterogeneous distributed systems. arXiv preprint arXiv:1603.04467 (2016)"},{"key":"8_CR2","doi-asserted-by":"crossref","unstructured":"Abe, A., Sumii, E.: A simple and practical linear algebra library interface with static size checking. arXiv preprint arXiv:1512.01898 (2015)","DOI":"10.4204\/EPTCS.198.1"},{"key":"8_CR3","unstructured":"contributors, H.: Hasktorch. http:\/\/hasktorch.org\/ (2020), [Online; accessed 15-July-2021]"},{"key":"8_CR4","unstructured":"contributors, O.T.: Ocaml-torch. https:\/\/github.com\/LaurentMazare\/ocaml-torch (2020), [Online; accessed 05-July-2021]"},{"key":"8_CR5","doi-asserted-by":"crossref","unstructured":"De\u00a0Moura, L., Bj\u00f8rner, N.: Z3: An efficient smt solver. In: International conference on Tools and Algorithms for the Construction and Analysis of Systems. pp. 337\u2013340. Springer (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"8_CR6","doi-asserted-by":"crossref","unstructured":"Dolby, J., Shinnar, A., Allain, A., Reinen, J.: Ariadne: analysis for machine learning programs. In: Proceedings of the 2Nd ACM SIGPLAN International Workshop on Machine Learning and Programming Languages. pp. 1\u201310 (2018)","DOI":"10.1145\/3211346.3211349"},{"key":"8_CR7","doi-asserted-by":"crossref","unstructured":"Eaton, F.: Statically typed linear algebra in haskell. In: Proceedings of the 2006 ACM SIGPLAN workshop on Haskell. pp. 120\u2013121 (2006)","DOI":"10.1145\/1159842.1159859"},{"key":"8_CR8","doi-asserted-by":"crossref","unstructured":"Eremondi, J., Tanter, \u00c9., Garcia, R.: Approximate normalization for gradual dependent types. Proceedings of the ACM on Programming Languages 3(ICFP), 1\u201330 (2019)","DOI":"10.1145\/3341692"},{"key":"8_CR9","doi-asserted-by":"crossref","unstructured":"Findler, R.B., Felleisen, M.: Contracts for higher-order functions. In: Proceedings of the seventh ACM SIGPLAN international conference on Functional programming. pp. 48\u201359 (2002)","DOI":"10.1145\/583852.581484"},{"key":"8_CR10","doi-asserted-by":"crossref","unstructured":"Freeman, T., Pfenning, F.: Refinement types for ml. In: Proceedings of the ACM SIGPLAN 1991 conference on Programming language design and implementation. pp. 268\u2013277 (1991)","DOI":"10.1145\/113446.113468"},{"key":"8_CR11","doi-asserted-by":"crossref","unstructured":"Garcia, R., Clark, A.M., Tanter, \u00c9.: Abstracting gradual typing. In: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. pp. 429\u2013442 (2016)","DOI":"10.1145\/2837614.2837670"},{"key":"8_CR12","doi-asserted-by":"crossref","unstructured":"Gibbons, J.: Aplicative programming with naperian functors. In: Proceedings of the 1st International Workshop on Type-Driven Development. pp. 13\u201314 (2016)","DOI":"10.1145\/2976022.2976023"},{"key":"8_CR13","doi-asserted-by":"crossref","unstructured":"Hattori, M., Kobayashi, N., Sato, R.: Gradual tensor shape checking. arXiv preprint arXiv:2203.08402 (2022)","DOI":"10.1007\/978-3-031-30044-8_8"},{"key":"8_CR14","doi-asserted-by":"crossref","unstructured":"Hattori, M., Sawada, S., Hamaji, S., Sakai, M., Shimizu, S.: Semi-static type, shape, and symbolic shape inference for dynamic computation graphs. In: Proceedings of the 4th ACM SIGPLAN International Workshop on Machine Learning and Programming Languages. pp. 11\u201319 (2020)","DOI":"10.1145\/3394450.3397465"},{"key":"8_CR15","doi-asserted-by":"crossref","unstructured":"Jhoo, H.Y., Kim, S., Song, W., Park, K., Lee, D., Yi, K.: A static analyzer for detecting tensor shape errors in deep neural network training code. arXiv preprint arXiv:2112.09037 (2021)","DOI":"10.1145\/3510454.3528638"},{"key":"8_CR16","doi-asserted-by":"publisher","unstructured":"Knowles, K., Flanagan, C.: Hybrid type checking. ACM Trans. Program. Lang. Syst. 32(2), 6:1\u20136:34 (2010). https:\/\/doi.org\/10.1145\/1667048.1667051","DOI":"10.1145\/1667048.1667051"},{"key":"8_CR17","unstructured":"Lagouvardos, S., Dolby, J., Grech, N., Antoniadis, A., Smaragdakis, Y.: Static analysis of shape in tensorflow programs. In: 34th European Conference on Object-Oriented Programming (ECOOP 2020). Schloss Dagstuhl-Leibniz-Zentrum f\u00fcr Informatik (2020)"},{"key":"8_CR18","doi-asserted-by":"crossref","unstructured":"Lehmann, N., Tanter, \u00c9.: Gradual refinement types. In: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages. pp. 775\u2013788 (2017)","DOI":"10.1145\/3009837.3009856"},{"key":"8_CR19","unstructured":"Meyer, B.: Eiffel: the language. Prentice-Hall, Inc. (1992)"},{"key":"8_CR20","unstructured":"Paszke, A., Gross, S., Chintala, S., Chanan, G., Yang, E., DeVito, Z., Lin, Z., Desmaison, A., Antiga, L., Lerer, A.: Automatic differentiation in pytorch (2017)"},{"key":"8_CR21","unstructured":"Paszke, A., Saeta, B.: Tensors fitting perfectly. arXiv preprint arXiv:2102.13254 (2021)"},{"key":"8_CR22","doi-asserted-by":"crossref","unstructured":"Prabhu, S., Fedyukovich, G., Madhukar, K., D\u2019Souza, D.: Specification synthesis with constrained horn clauses. In: Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation. pp. 1203\u20131217 (2021)","DOI":"10.1145\/3453483.3454104"},{"key":"8_CR23","doi-asserted-by":"crossref","unstructured":"Rastogi, A., Swamy, N., Fournet, C., Bierman, G., Vekris, P.: Safe & efficient gradual typing for typescript. In: Proceedings of the 42Nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. pp. 167\u2013180 (2015)","DOI":"10.1145\/2676726.2676971"},{"key":"8_CR24","unstructured":"Roesch, J., Lyubomirsky, S., Kirisame, M., Weber, L., Pollock, J., Vega, L., Jiang, Z., Chen, T., Moreau, T., Tatlock, Z.: Relay: A high-level compiler for deep learning. arXiv preprint arXiv:1904.08368 (2019)"},{"key":"8_CR25","doi-asserted-by":"crossref","unstructured":"Roesch, J., Lyubomirsky, S., Weber, L., Pollock, J., Kirisame, M., Chen, T., Tatlock, Z.: Relay: A new ir for machine learning frameworks. In: Proceedings of the 2nd ACM SIGPLAN International Workshop on Machine Learning and Programming Languages. pp. 58\u201368 (2018)","DOI":"10.1145\/3211346.3211348"},{"key":"8_CR26","doi-asserted-by":"crossref","unstructured":"Rondon, P.M., Kawaguci, M., Jhala, R.: Liquid types. In: Proceedings of the 29th ACM SIGPLAN Conference on Programming Language Design and Implementation. pp. 159\u2013169 (2008)","DOI":"10.1145\/1375581.1375602"},{"key":"8_CR27","unstructured":"Siek, J.G., Vitousek, M.M., Cimini, M., Boyland, J.T.: Refined criteria for gradual typing. In: 1st Summit on Advances in Programming Languages (SNAPL 2015). Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik (2015)"},{"key":"8_CR28","doi-asserted-by":"crossref","unstructured":"Slepak, J., Manolios, P., Shivers, O.: Rank polymorphism viewed as a constraint problem. In: Proceedings of the 5th ACM SIGPLAN International Workshop on Libraries, Languages, and Compilers for Array Programming. pp. 34\u201341 (2018)","DOI":"10.1145\/3219753.3219758"},{"key":"8_CR29","doi-asserted-by":"crossref","unstructured":"Slepak, J., Shivers, O., Manolios, P.: An array-oriented language with static rank polymorphism. In: European Symposium on Programming Languages and Systems. pp. 27\u201346. Springer (2014)","DOI":"10.1007\/978-3-642-54833-8_3"},{"key":"8_CR30","doi-asserted-by":"crossref","unstructured":"Vazou, N., Tanter, \u00c9., Van\u00a0Horn, D.: Gradual liquid type inference. Proceedings of the ACM on Programming Languages 2(OOPSLA), 1\u201325 (2018)","DOI":"10.1145\/3276502"},{"key":"8_CR31","unstructured":"Verma, S., Su, Z.: Shapeflow: Dynamic shape interpreter for tensorflow. arXiv preprint arXiv:2011.13452 (2020)"},{"key":"8_CR32","doi-asserted-by":"crossref","unstructured":"Wadler, P., Findler, R.B.: Well-typed programs can\u2019t be blamed. In: European Symposium on Programming. pp. 1\u201316. Springer (2009)","DOI":"10.1007\/978-3-642-00590-9_1"},{"key":"8_CR33","doi-asserted-by":"crossref","unstructured":"Xi, H., Pfenning, F.: Eliminating array bound checking through dependent types. In: Proceedings of the ACM SIGPLAN 1998 conference on Programming language design and implementation. pp. 249\u2013257 (1998)","DOI":"10.1145\/277652.277732"},{"key":"8_CR34","doi-asserted-by":"crossref","unstructured":"Xi, H., Pfenning, F.: Dependent types in practical programming. In: Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages. pp. 214\u2013227 (1999)","DOI":"10.1145\/292540.292560"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-30044-8_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,6,7]],"date-time":"2023-06-07T09:03:59Z","timestamp":1686128639000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-30044-8_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031300431","9783031300448"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-30044-8_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"17 April 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ESOP","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"European Symposium on Programming","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":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 April 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 April 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"32","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"esop2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2023\/esop","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-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":"55","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":"20","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":"0","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":"36% - 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","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":"5.5","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":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}