{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,1]],"date-time":"2025-05-01T16:10:54Z","timestamp":1746115854110,"version":"3.40.4"},"publisher-location":"Cham","reference-count":27,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031911170"},{"type":"electronic","value":"9783031911187"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,5,1]],"date-time":"2025-05-01T00:00:00Z","timestamp":1746057600000},"content-version":"vor","delay-in-days":120,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>Dependent pattern matching is a key feature in dependently typed programming. However, there is a theory-practice disconnect: while many proof assistants implement pattern matching as primitive, theoretical presentations give semantics to pattern matching by elaborating to eliminators. Though theoretically convenient, eliminators can be awkward and verbose, particularly for complex combinations of patterns.<\/jats:p>\n          <jats:p>This work aims to bridge the theory-practice gap by presenting a direct categorical semantics for pattern matching, which does not elaborate to eliminators. This is achieved using sheaf theory to describe when sets of arrows (terms) can be amalgamated into a single arrow. We present a language with top-level dependent pattern matching, without specifying which sets of patterns are considered covering for a match. Then, we give a sufficient criterion for which pattern-sets admit a sound model: patterns should be in the canonical coverage for the category of contexts. Finally, we use sheaf-theoretic saturation conditions to devise some allowable sets of patterns. We are able to express and exceed the status quo, giving semantics for datatype constructors, nested patterns, absurd patterns, propositional equality, and dot patterns.<\/jats:p>","DOI":"10.1007\/978-3-031-91118-7_11","type":"book-chapter","created":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T08:17:06Z","timestamp":1746001026000},"page":"264-291","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Coverage Semantics for Dependent Pattern Matching"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-9631-4826","authenticated-orcid":false,"given":"Joseph","family":"Eremondi","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2071-0929","authenticated-orcid":false,"given":"Ohad","family":"Kammar","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,5,1]]},"reference":[{"key":"11_CR1","doi-asserted-by":"publisher","unstructured":"Abbott, M., Altenkirch, T., Ghani, N.: Containers: Constructing strictly positive types. Theor. Comput. Sci. 342(1), 3\u201327 (2005), ISSN 0304-3975, https:\/\/doi.org\/10.1016\/j.tcs.2005.06.002","DOI":"10.1016\/j.tcs.2005.06.002"},{"key":"11_CR2","doi-asserted-by":"publisher","unstructured":"Altenkirch, T., Ghani, N., Hancock, P., Mcbride, C., Morris, P.: Indexed containers. J. Funct. Program. 25, e5 (Jan 2015), ISSN 0956-7968, 1469-7653, https:\/\/doi.org\/10.1017\/S095679681500009X","DOI":"10.1017\/S095679681500009X"},{"key":"11_CR3","doi-asserted-by":"publisher","unstructured":"Annenkov, D., Capriotti, P., Kraus, N., Sattler, C.: Two-level type theory and applications. Math. Struct. Comput. Sci. 33(8), 688\u2013743 (Sep 2023), ISSN 0960-1295, 1469-8072, https:\/\/doi.org\/10.1017\/S0960129523000130","DOI":"10.1017\/S0960129523000130"},{"key":"11_CR4","doi-asserted-by":"crossref","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development. Springer-Verlag (2004)","DOI":"10.1007\/978-3-662-07964-5"},{"key":"11_CR5","doi-asserted-by":"publisher","unstructured":"Brady, E.: Idris 2: Quantitative Type Theory in Practice. In: 35th Eur. Conf. Object-Oriented Program. ECOOP 2021, Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik (2021), https:\/\/doi.org\/10.4230\/LIPIcs.ECOOP.2021.9","DOI":"10.4230\/LIPIcs.ECOOP.2021.9"},{"key":"11_CR6","doi-asserted-by":"publisher","unstructured":"Cockx, J., Devriese, D., Piessens, F.: Pattern matching without K. In: Proc. 19th ACM SIGPLAN Int. Conf. Funct. Program., pp. 257\u2013268, ICFP \u201914, ACM, New York, NY, USA (2014), ISBN 978-1-4503-2873-9, https:\/\/doi.org\/10.1145\/2628136.2628139","DOI":"10.1145\/2628136.2628139"},{"key":"11_CR7","doi-asserted-by":"publisher","unstructured":"Cockx, J., Piessens, F., Devriese, D.: Overlapping and Order-Independent Patterns. In: Shao, Z. (ed.) Program. Lang. Syst., pp. 87\u2013106, Springer, Berlin, Heidelberg (2014), ISBN 978-3-642-54833-8, https:\/\/doi.org\/10.1007\/978-3-642-54833-8_6","DOI":"10.1007\/978-3-642-54833-8_6"},{"key":"11_CR8","doi-asserted-by":"publisher","unstructured":"Cohen, C., Coquand, T., Huber, S., M\u00f6rtberg, A.: Cubical type theory: A constructive interpretation of the univalence axiom. In: Uustalu, T. (ed.) 21st Int. Conf. Types Proofs Programs TYPES 2015, Leibniz International Proceedings in Informatics (LIPIcs), vol.\u00a069, pp. 5:1\u20135:34, Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany (2018), ISBN 978-3-95977-030-9, ISSN 1868-8969, https:\/\/doi.org\/10.4230\/LIPIcs.TYPES.2015.5","DOI":"10.4230\/LIPIcs.TYPES.2015.5"},{"key":"11_CR9","unstructured":"Coquand, T.: Pattern matching with dependent types. In: Informal Proc. Log. Framew., vol.\u00a092, pp. 66\u201379 (1992)"},{"key":"11_CR10","unstructured":"Documentation for Agda: Data.Vec.Base. https:\/\/github.com\/agda\/agda-stdlib\/blob\/196766082e913de0d7cd98e3b672935a3b4528b8\/src\/Data\/Vec\/Base.agda (2024)"},{"key":"11_CR11","doi-asserted-by":"publisher","unstructured":"Eremondi, J.: Joeyeremondi\/lean-cwf: Lean proof for esop 2025 \"coverage semantics for dependent pattern matching\" (Jan 2025), https:\/\/doi.org\/10.5281\/zenodo.14768609, URL https:\/\/doi.org\/10.5281\/zenodo.14768609","DOI":"10.5281\/zenodo.14768609"},{"key":"11_CR12","doi-asserted-by":"publisher","unstructured":"Goguen, H., McBride, C., McKinna, J.: Eliminating dependent pattern matching. In: Futatsugi, K., Jouannaud, J.P., Meseguer, J. (eds.) Algebra, Meaning, and Computation: Essays Dedicated to Joseph A. Goguen on the Occasion of His 65th Birthday, pp. 521\u2013540, Springer Berlin Heidelberg, Berlin, Heidelberg (2006), ISBN 978-3-540-35464-2, https:\/\/doi.org\/10.1007\/11780274_27","DOI":"10.1007\/11780274_27"},{"key":"11_CR13","doi-asserted-by":"crossref","unstructured":"Goguen, J.A.: What is unification?: A categorical view of substitution, equation and solution. In: Algebraic Techniques, pp. 217\u2013261, Elsevier (1989)","DOI":"10.1016\/B978-0-12-046370-1.50012-7"},{"key":"11_CR14","doi-asserted-by":"publisher","unstructured":"Hofmann, M.: Syntax and Semantics of Dependent Types. In: Pitts, A.M., Dybjer, P. (eds.) Semantics and Logics of Computation, pp. 79\u2013130, Publications of the Newton Institute, Cambridge University Press, Cambridge (1997), ISBN 978-0-521-58057-1, https:\/\/doi.org\/10.1017\/CBO9780511526619.004","DOI":"10.1017\/CBO9780511526619.004"},{"key":"11_CR15","unstructured":"Johnstone, P.T.: Sketches of an Elephant: A Topos Theory Compendium. Oxford Logic Guides, Oxford University Press, Oxford, New York (Jul 2003), ISBN 978-0-19-852496-0"},{"key":"11_CR16","unstructured":"Lurie, J.: Higher Topos Theory. No. no. 170 in Annals of Mathematics Studies, Princeton University Press, Princeton, N.J (2009), ISBN 978-0-691-14048-3 978-0-691-14049-0"},{"key":"11_CR17","unstructured":"MacLane, S., Moerdijk, I.: Sheaves in Geometry and Logic: A First Introduction to Topos Theory. Springer, New York, NY, UNITED STATES (1992), ISBN 978-1-4612-0927-0"},{"key":"11_CR18","unstructured":"McBride, C.: Dependently Typed Functional Programs and Their Proofs. Ph.D. thesis, University of Edinburgh, UK (2000)"},{"key":"11_CR19","doi-asserted-by":"publisher","unstructured":"McBride, C.: Elimination with a Motive. In: Callaghan, P., Luo, Z., McKinna, J., Pollack, R., Pollack, R. (eds.) Types Proofs Programs, pp. 197\u2013216, Lecture Notes in Computer Science, Springer, Berlin, Heidelberg (2002), ISBN 978-3-540-45842-5, https:\/\/doi.org\/10.1007\/3-540-45842-5_13","DOI":"10.1007\/3-540-45842-5_13"},{"key":"11_CR20","doi-asserted-by":"publisher","unstructured":"McBride, C.: Epigram: Practical Programming with Dependent Types. In: Vene, V., Uustalu, T. (eds.) Adv. Funct. Program., pp. 130\u2013170, Springer, Berlin, Heidelberg (2005), ISBN 978-3-540-31872-9, https:\/\/doi.org\/10.1007\/11546382_3","DOI":"10.1007\/11546382_3"},{"key":"11_CR21","doi-asserted-by":"publisher","unstructured":"Mcbride, C., Mckinna, J.: The view from the left. J. Funct. Prog. 14(1), 69\u2013111 (Jan 2004), ISSN 0956-7968, 1469-7653, https:\/\/doi.org\/10.1017\/S0956796803004829","DOI":"10.1017\/S0956796803004829"},{"key":"11_CR22","doi-asserted-by":"publisher","unstructured":"Norell, U.: Dependently typed programming in Agda. In: Proc. 4th Int. Workshop Types Lang. Des. Implement., pp. 1\u20132, TLDI \u201909, ACM, New York, NY, USA (2009), ISBN 978-1-60558-420-1, https:\/\/doi.org\/10.1145\/1481861.1481862","DOI":"10.1145\/1481861.1481862"},{"key":"11_CR23","unstructured":"Rydeheard, D.E., Burstall, R.M.: Computational category theory. Prentice Hall International (UK) Ltd., GBR (1988), ISBN 0131627368"},{"key":"11_CR24","unstructured":"Sherman, B.: Making Discrete Decisions Based on Continuous Values. Master of Science, Massachusetts Institute of Technology (2017)"},{"key":"11_CR25","doi-asserted-by":"publisher","unstructured":"Sherman, B., Sciarappa, L., Chlipala, A., Carbin, M.: Computable decision making on the reals and other spaces: Via partiality and nondeterminism. In: Proc. 33rd Annu. ACMIEEE Symp. Log. Comput. Sci., pp. 859\u2013868, ACM, Oxford United Kingdom (Jul 2018), ISBN 978-1-4503-5583-4, https:\/\/doi.org\/10.1145\/3209108.3209193","DOI":"10.1145\/3209108.3209193"},{"key":"11_CR26","unstructured":"Univalent Foundations\u00a0Program, T.: Homotopy Type Theory: Univalent Foundations of Mathematics. https:\/\/homotopytypetheory.org\/book, Institute for Advanced Study (2013)"},{"key":"11_CR27","doi-asserted-by":"publisher","unstructured":"Wadler, P.: Views: A way for pattern matching to cohabit with data abstraction. In: Proc. 14th ACM SIGACT-SIGPLAN Symp. Princ. Program. Lang., pp. 307\u2013313, POPL \u201987, Association for Computing Machinery, New York, NY, USA (Oct 1987), ISBN 978-0-89791-215-0, https:\/\/doi.org\/10.1145\/41625.41653","DOI":"10.1145\/41625.41653"}],"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-91118-7_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T08:17:16Z","timestamp":1746001036000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-91118-7_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031911170","9783031911187"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-91118-7_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"1 May 2025","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":"Hamilton, ON","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Canada","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3 May 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 May 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"34","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"esop2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2025\/conferences\/esop\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}