{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,11]],"date-time":"2026-05-11T17:27:25Z","timestamp":1778520445361,"version":"3.51.4"},"publisher-location":"New York, NY, USA","reference-count":41,"publisher":"ACM","license":[{"start":{"date-parts":[[2023,8,29]],"date-time":"2023-08-29T00:00:00Z","timestamp":1693267200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2023,8,29]]},"DOI":"10.1145\/3652561.3652572","type":"proceedings-article","created":{"date-parts":[[2024,6,19]],"date-time":"2024-06-19T18:19:52Z","timestamp":1718821192000},"page":"1-14","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["Type Patterns: Pattern Matching on Shape-Carrying Array Types"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0009-0001-3018-5152","authenticated-orcid":false,"given":"Jordy","family":"Aaldering","sequence":"first","affiliation":[{"name":"Dept. Software Science, Radboud University, Netherlands"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8663-1043","authenticated-orcid":false,"given":"Sven-Bodo","family":"Scholz","sequence":"additional","affiliation":[{"name":"Dept. Software Science, Radboud University, Netherlands"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0974-4634","authenticated-orcid":false,"given":"Bernard Van","family":"Gastel","sequence":"additional","affiliation":[{"name":"Dept. Software Science, Radboud University, Netherlands"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2024,6,19]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"Zachary\u00a0Ryan Anderson. 2007. Static analysis of C for hybrid type checking. Technical Report. Tech. Rep. EECS-2007-1 UC Berkeley."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/289423.289451"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3609024.3609412"},{"key":"e_1_3_2_1_4_1","volume-title":"Construction and Analysis of Safe, Secure, and Interoperable Smart Devices, Gilles Barthe, Lilian Burdy, Marieke Huisman, Jean-Louis Lanet","author":"Barnett Mike","unstructured":"Mike Barnett, K.\u00a0Rustan\u00a0M. Leino, and Wolfram Schulte. 2005. The Spec# Programming System: An Overview. In Construction and Analysis of Safe, Secure, and Interoperable Smart Devices, Gilles Barthe, Lilian Burdy, Marieke Huisman, Jean-Louis Lanet, and Traian Muntean (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 49\u201369."},{"key":"e_1_3_2_1_5_1","volume-title":"Implementation and Application of Functional Languages, Marco\u00a0T","author":"Bernecky Robert","unstructured":"Robert Bernecky, Stephan Herhut, and Sven-Bodo Scholz. 2010. Symbiotic Expressions. In Implementation and Application of Functional Languages, Marco\u00a0T. Moraz\u00e1n and Sven-Bodo Scholz (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 107\u2013124."},{"key":"e_1_3_2_1_6_1","volume-title":"Theorem Proving in Higher Order Logics","author":"Bove Ana","unstructured":"Ana Bove, Peter Dybjer, and Ulf Norell. 2009. A Brief Overview of Agda - A Functional Language with Dependent Types. In Theorem Proving in Higher Order Logics, Stefan Berghofer, Tobias Nipkow, Christian Urban, and Makarius Wenzel (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 73\u201378."},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1929529.1929536"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.6092\/issn.1972-5787\/1978"},{"key":"e_1_3_2_1_9_1","volume-title":"Dependent Types for Low-Level Programming","author":"Condit Jeremy","unstructured":"Jeremy Condit, Matthew Harren, Zachary Anderson, David Gay, and George\u00a0C. Necula. 2007. Dependent Types for Low-Level Programming. In Programming Languages and Systems, Rocco De\u00a0Nicola (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 520\u2013535."},{"key":"e_1_3_2_1_10_1","volume-title":"The yices smt solver. Tool paper at http:\/\/yices. csl. sri. com\/tool-paper. pdf 2, 2","author":"Dutertre Bruno","year":"2006","unstructured":"Bruno Dutertre and Leonardo De\u00a0Moura. 2006. The yices smt solver. Tool paper at http:\/\/yices. csl. sri. com\/tool-paper. pdf 2, 2 (2006), 1\u20132."},{"key":"e_1_3_2_1_11_1","volume-title":"Non-Linear Pattern-Matching against Unfree Data Types with Lexical Scoping. CoRR abs\/1407.0729","author":"Egi Satoshi","year":"2014","unstructured":"Satoshi Egi. 2014. Non-Linear Pattern-Matching against Unfree Data Types with Lexical Scoping. CoRR abs\/1407.0729 (2014). arXiv:1407.0729http:\/\/arxiv.org\/abs\/1407.0729"},{"key":"e_1_3_2_1_12_1","volume-title":"Non-linear Pattern Matching with Backtracking for Non-free Data Types","author":"Egi Satoshi","unstructured":"Satoshi Egi and Yuichi Nishiwaki. 2018. Non-linear Pattern Matching with Backtracking for Non-free Data Types. In Programming Languages and Systems, Sukyoung Ryu (Ed.). Springer International Publishing, Cham, 3\u201323."},{"key":"e_1_3_2_1_13_1","volume-title":"Implementation of Functional Languages","author":"Erwig Martin","unstructured":"Martin Erwig. 1997. Active patterns. In Implementation of Functional Languages, Werner Kluge (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 21\u201340."},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111059"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/113445.113468"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-32096-5_5"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10766-006-0018-x"},{"key":"e_1_3_2_1_18_1","volume-title":"Towards Hybrid Array Types in SaC. In Software Engineering (Workshops)(CEUR Workshop Proceedings), Vol.\u00a01129","author":"Grelck Clemens","year":"2014","unstructured":"Clemens Grelck, Fangyong Tang, 2014. Towards Hybrid Array Types in SaC. In Software Engineering (Workshops)(CEUR Workshop Proceedings), Vol.\u00a01129. CEUR-WS.org, 129\u2013145. https:\/\/ceur-ws.org\/Vol-1129\/paper44.pdf"},{"key":"e_1_3_2_1_19_1","volume-title":"Scheme and Functional Programming Workshop, Vol.\u00a06. 93\u2013104","author":"Gronski Jessica","year":"2006","unstructured":"Jessica Gronski, Kenneth Knowles, Aaron Tomb, Stephen\u00a0N Freund, and Cormac Flanagan. 2006. Sage: Hybrid checking for flexible specifications. In Scheme and Functional Programming Workshop, Vol.\u00a06. 93\u2013104."},{"key":"e_1_3_2_1_20_1","volume-title":"Cyclone: A type-safe dialect of C. C\/C++ Users Journal 23, 1","author":"Grossman Dan","year":"2005","unstructured":"Dan Grossman, Michael Hicks, Trevor Jim, and Greg Morrisett. 2005. Cyclone: A type-safe dialect of C. C\/C++ Users Journal 23, 1 (2005), 112\u2013139."},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3460944.3464310"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062354"},{"key":"e_1_3_2_1_23_1","volume-title":"Implementation and Application of Functional Languages, Olaf Chitil, Zolt\u00e1n Horv\u00e1th, and Vikt\u00f3ria Zs\u00f3k (Eds.)","author":"Herhut Stephan","unstructured":"Stephan Herhut, Sven-Bodo Scholz, Robert Bernecky, Clemens Grelck, and Kai Trojahner. 2008. From Contracts Towards Dependent Types: Proofs by Partial Evaluation. In Implementation and Application of Functional Languages, Olaf Chitil, Zolt\u00e1n Horv\u00e1th, and Vikt\u00f3ria Zs\u00f3k (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 254\u2013273."},{"key":"e_1_3_2_1_24_1","unstructured":"C\u00a0Barry Jay and Milan Sekanina. 1996. Shape checking of array programs. Technical Report. Citeseer."},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3426422.3426983"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503286"},{"key":"e_1_3_2_1_27_1","volume-title":"Exploring New Frontiers of Theoretical Informatics, Jean-Jacques Levy, Ernst\u00a0W","author":"Ou Xinming","unstructured":"Xinming Ou, Gang Tan, Yitzhak Mandelbaum, and David Walker. 2004. Dynamic Typing with Dependent Types. In Exploring New Frontiers of Theoretical Informatics, Jean-Jacques Levy, Ernst\u00a0W. Mayr, and John\u00a0C. Mitchell (Eds.). Springer US, Boston, MA, 437\u2013450."},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328408.1328434"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796802004458"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3412932.3412947"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3219753.3219758"},{"key":"e_1_3_2_1_32_1","volume-title":"An Array-Oriented Language with Static Rank Polymorphism","author":"Slepak Justin","unstructured":"Justin Slepak, Olin Shivers, and Panagiotis Manolios. 2014. An Array-Oriented Language with Static Rank Polymorphism. In Programming Languages and Systems, Zhong Shao (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 27\u201346."},{"key":"e_1_3_2_1_33_1","volume-title":"DRAFT PROCEEDINGS OF THE 24TH SYMPOSIUM ON IMPLEMENTATION AND APPLICATION OF FUNCTIONAL LANGUAGES (IFL","author":"Tang Fangyong","year":"2012","unstructured":"Fangyong Tang, Clemens Grelck, 2012. User-defined shape constraints in SaC. In DRAFT PROCEEDINGS OF THE 24TH SYMPOSIUM ON IMPLEMENTATION AND APPLICATION OF FUNCTIONAL LANGUAGES (IFL 2012). 416\u2013434."},{"key":"e_1_3_2_1_34_1","volume-title":"QUBE-Array Programming with Dependent Types","author":"Trojahner Kai","unstructured":"Kai Trojahner. 2011. QUBE-Array Programming with Dependent Types. Institute of Software Engineering and Programming Languages of the University of L\u00fcbeck (2011)."},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2009.03.002"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-46559-3_2"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.248.7"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/277650.277732"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/292540.292560"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(97)00062-5"},{"key":"e_1_3_2_1_41_1","volume-title":"Verification, Model Checking, and Abstract Interpretation, Deepak D\u2019Souza, Akash Lal, and Kim\u00a0Guldstrand Larsen (Eds.)","author":"Zhu He","unstructured":"He Zhu, Aditya\u00a0V. Nori, and Suresh Jagannathan. 2015. Dependent Array Type Inference from Tests. In Verification, Model Checking, and Abstract Interpretation, Deepak D\u2019Souza, Akash Lal, and Kim\u00a0Guldstrand Larsen (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 412\u2013430."}],"event":{"name":"IFL 2023: The 35th Symposium on Implementation and Application of Functional Languages","location":"Braga Portugal","acronym":"IFL 2023"},"container-title":["The 35th Symposium on Implementation and Application of Functional Languages"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3652561.3652572","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3652561.3652572","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,26]],"date-time":"2025-08-26T19:10:58Z","timestamp":1756235458000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3652561.3652572"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,8,29]]},"references-count":41,"alternative-id":["10.1145\/3652561.3652572","10.1145\/3652561"],"URL":"https:\/\/doi.org\/10.1145\/3652561.3652572","relation":{},"subject":[],"published":{"date-parts":[[2023,8,29]]},"assertion":[{"value":"2024-06-19","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}