{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,26]],"date-time":"2026-05-26T23:06:00Z","timestamp":1779836760589,"version":"3.53.1"},"reference-count":38,"publisher":"Cambridge University Press (CUP)","license":[{"start":{"date-parts":[[2020,1,21]],"date-time":"2020-01-21T00:00:00Z","timestamp":1579564800000},"content-version":"unspecified","delay-in-days":20,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[2020]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    In a dependently typed language, we can guarantee correctness of our programmes by providing formal proofs. To check them, the typechecker elaborates these programs and proofs into a low-level core language. However, this core language is by nature hard to understand by mere humans, so how can we know we proved the right thing? This question occurs in particular for dependent copattern matching, a powerful language construct for writing programmes and proofs by dependent case analysis and mixed induction\/coinduction. A definition by copattern matching consists of a list of\n                    <jats:italic>clauses<\/jats:italic>\n                    that are elaborated to a\n                    <jats:italic>case tree<\/jats:italic>\n                    , which can be further translated to primitive\n                    <jats:italic>eliminators<\/jats:italic>\n                    . In previous work this second step has received a lot of attention, but the first step has been mostly ignored so far. We present an algorithm elaborating definitions by dependent copattern matching to a core language with inductive data types, coinductive record types, an identity type, and constants defined by well-typed case trees. To ensure correctness, we prove that elaboration preserves the first-match semantics of the user clauses. Based on this theoretical work, we reimplement the algorithm used by Agda to check left-hand sides of definitions by pattern matching. The new implementation is at the same time more general and less complex, and fixes a number of bugs and usability issues with the old version. Thus, we take another step towards the formally verified implementation of a practical dependently typed language.\n                  <\/jats:p>","DOI":"10.1017\/s0956796819000182","type":"journal-article","created":{"date-parts":[[2020,1,21]],"date-time":"2020-01-21T02:37:31Z","timestamp":1579574251000},"source":"Crossref","is-referenced-by-count":1,"title":["Elaborating dependent (co)pattern matching: No pattern left behind"],"prefix":"10.1017","volume":"30","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-3862-4073","authenticated-orcid":false,"given":"JESPER","family":"COCKX","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"ANDREAS","family":"ABEL","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"56","published-online":{"date-parts":[[2020,1,21]]},"reference":[{"key":"S0956796819000182_ref38","unstructured":"Zeilberger, N. (2009) The Logical Basis of Evaluation Order and Pattern-Matching. PhD thesis, Carnegie Mellon University. Available at: http:\/\/software.imdea.org\/~noam.zeilberger\/thesis.pdf"},{"key":"S0956796819000182_ref36","unstructured":"Thibodeau, D. , Cave, A. & Pientka, B. (2016) Indexed codata types. In Garrigue et al. (2016), pp. 351\u2013363. Available at: http:\/\/doi.acm.org\/10.1145\/2951913.2951929"},{"key":"S0956796819000182_ref35","doi-asserted-by":"crossref","unstructured":"Sozeau, M. (2010) Equations: A dependent pattern-matching compiler. In Interactive Theorem Proving, First International Conference, ITP 2010, Edinburgh, UK, July 11\u201314, 2010. Proceedings, Kaufmann, M. & Paulson, L. C. (eds), vol. 6172. Lecture Notes in Computer Science. Springer, pp. 419\u2013434. Available at: https:\/\/doi.org\/10.1007\/978-3-642-14052-5_29","DOI":"10.1007\/978-3-642-14052-5_29"},{"key":"S0956796819000182_ref33","doi-asserted-by":"publisher","DOI":"10.7146\/brics.v4i18.18945"},{"key":"S0956796819000182_ref31","unstructured":"Norell, U. (2007) Towards a practical programming language based on dependent type theory. PhD thesis, Chalmers University of Technology."},{"key":"S0956796819000182_ref30","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796803004829"},{"key":"S0956796819000182_ref28","doi-asserted-by":"publisher","DOI":"10.1145\/141471.141499"},{"key":"S0956796819000182_ref26","doi-asserted-by":"publisher","DOI":"10.1145\/3131851.3131869"},{"key":"S0956796819000182_ref29","unstructured":"McBride, C. (2000) Dependently typed functional programs and their proofs. PhD thesis, University of Edinburgh."},{"key":"S0956796819000182_ref27","doi-asserted-by":"crossref","unstructured":"Licata, D. R. , Zeilberger, N. & Harper, R. (2008) Focusing on binding and computation. In Proceedings of the Twenty-Third Annual IEEE Symposium on Logic in Computer Science, LICS 2008, 24\u201327 June 2008, Pittsburgh, PA, USA, Pfenning, F. (ed). IEEE Computer Society Press, pp. 241\u2013252. Available at: https:\/\/doi.org\/10.1109\/LICS.2008.48","DOI":"10.1109\/LICS.2008.48"},{"key":"S0956796819000182_ref25","doi-asserted-by":"publisher","DOI":"10.1145\/1594834.1480927"},{"key":"S0956796819000182_ref9","unstructured":"Agda issue. (2018b) Mismatch between order of matching in clauses and case tree; subject reduction broken. Available at: https:\/\/github.com\/agda\/agda\/issues\/2964. (on the Agda bug tracker)."},{"key":"S0956796819000182_ref23","doi-asserted-by":"publisher","DOI":"10.1007\/11780274_27"},{"key":"S0956796819000182_ref3","unstructured":"Agda development team. (2017) Agda 2.5.3 documentation. Available at: http:\/\/agda.readthedocs.io\/en\/v2.5.3\/"},{"key":"S0956796819000182_ref6","unstructured":"Agda issue (2017c). Panic: Unbound variable. Available at: https:\/\/github.com\/agda\/agda\/issues\/2856 (on the Agda bug tracker)."},{"key":"S0956796819000182_ref5","unstructured":"Agda issue. (2017b) Record constructor is accepted, record pattern is not. Available at: https:\/\/github.com\/agda\/agda\/issues\/2850 (on the Agda bug tracker)."},{"key":"S0956796819000182_ref1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500591"},{"key":"S0956796819000182_ref2","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429075"},{"key":"S0956796819000182_ref10","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/2.3.297"},{"key":"S0956796819000182_ref16","unstructured":"Cockx, J. (2017) Dependent pattern matching and proof-relevant unification. PhD thesis, KU Leuven, 2017."},{"key":"S0956796819000182_ref32","doi-asserted-by":"publisher","DOI":"10.1145\/1292597.1292606"},{"key":"S0956796819000182_ref21","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21401-6_26"},{"key":"S0956796819000182_ref4","unstructured":"Agda issue. (2017a) Disambiguation of type based on pattern leads to non-unique meta solution. Available at: https:\/\/github.com\/agda\/agda\/issues\/2834 (on the Agda bug tracker)."},{"key":"S0956796819000182_ref11","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-15975-4_48"},{"key":"S0956796819000182_ref12","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_5"},{"key":"S0956796819000182_ref7","unstructured":"Agda issue. (2017d) Internal error in src\/full\/agda\/typechecking\/coverage\/match.hs:312. Available at: https:\/\/github.com\/agda\/agda\/issues\/2874. (on the Agda bug tracker)."},{"key":"S0956796819000182_ref22","unstructured":"Garrigue, J. , Keller, G. & Sumii, E. (eds). Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, ICFP 2016, Nara, Japan, September 18\u201322, 2016. ACM Press. Available at: http:\/\/doi.acm.org\/10.1145\/2951913"},{"key":"S0956796819000182_ref13","doi-asserted-by":"publisher","DOI":"10.1017\/S095679681300018X"},{"key":"S0956796819000182_ref37","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328482"},{"key":"S0956796819000182_ref8","unstructured":"Agda issue. (2018a) Unifier throws away pattern. Available at: https:\/\/github.com\/agda\/agda\/issues\/2896. (on the Agda bug tracker)."},{"key":"S0956796819000182_ref14","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24849-1_8"},{"key":"S0956796819000182_ref24","volume-title":"The Coq Proof Assistant Reference Manual","year":"2017"},{"key":"S0956796819000182_ref15","doi-asserted-by":"publisher","DOI":"10.1145\/800055.802037"},{"key":"S0956796819000182_ref17","first-page":"1","article-title":"Elaborating dependent (co)pattern matching","volume":"2","author":"Cockx","year":"2018","journal-title":"PACMPL"},{"key":"S0956796819000182_ref19","unstructured":"Coquand, T. (1992) Pattern matching with dependent types. In Proceedings of the 1992 Workshop on Types for Proofs and Programs, B\u00e5stad, Sweden, June 1992, Nordstr\u00f6m, B. , Pettersson, K. & Plotkin, G. (eds). Chalmers University of Technology, pp. 71\u201383, 1992. Available at: http:\/\/www.cse.chalmers.se\/~coquand\/pattern.ps"},{"key":"S0956796819000182_ref18","unstructured":"Cockx, J. , Devriese, D. & Piessens, F. (2016) Unifiers as equivalences: Proof-relevant unification of dependently typed data. In Garrigue et al.(2016), pp. 270\u2013283. Available at: http:\/\/doi.acm.org\/10.1145\/2951913.2951917."},{"key":"S0956796819000182_ref34","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08918-8_3"},{"key":"S0956796819000182_ref20","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90066-B"}],"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0956796819000182","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,5,26]],"date-time":"2026-05-26T22:36:50Z","timestamp":1779835010000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0956796819000182\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"references-count":38,"alternative-id":["S0956796819000182"],"URL":"https:\/\/doi.org\/10.1017\/s0956796819000182","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"value":"0956-7968","type":"print"},{"value":"1469-7653","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020]]},"article-number":"e2"}}