{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,16]],"date-time":"2025-06-16T15:31:28Z","timestamp":1750087888179,"version":"3.40.5"},"reference-count":37,"publisher":"Cambridge University Press (CUP)","license":[{"start":{"date-parts":[[2023,1,24]],"date-time":"2023-01-24T00:00:00Z","timestamp":1674518400000},"content-version":"unspecified","delay-in-days":23,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["cambridge.org"],"crossmark-restriction":true},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[2023]]},"abstract":"<jats:title>Abstract<\/jats:title>\n\t  <jats:p>Contemporary proof assistants such as Coq require that recursive functions be terminating and corecursive functions be productive to maintain logical consistency of their type theories, and some ensure these properties using syntactic checks. However, being syntactic, they are inherently delicate and restrictive, preventing users from easily writing obviously terminating or productive functions at their whim.<\/jats:p>\n\t  <jats:p>Meanwhile, there exist many <jats:italic>sized type theories<\/jats:italic> that perform type-based termination and productivity checking, including theories based on the Calculus of (Co)Inductive Constructions (CIC), the core calculus underlying Coq. These theories are more robust and compositional in comparison. So why haven\u2019t they been adapted to Coq?<\/jats:p>\n\t  <jats:p>In this paper, we venture to answer this question with CIC<jats:inline-formula>\n\t      <jats:alternatives>\n\t\t<jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"png\" xlink:href=\"S0956796822000120_inline1.png\"\/>\n\t\t<jats:tex-math>\n$\\widehat{\\ast}$\n<\/jats:tex-math>\n\t      <\/jats:alternatives>\n\t    <\/jats:inline-formula>, a sized type theory based on CIC. It extends past work on sized types in CIC with additional Coq features such as global and local definitions. We also present a corresponding size inference algorithm and implement it within Coq\u2019s kernel; for maximal backward compatibility with existing Coq developments, it requires no additional annotations from the user.<\/jats:p>\n\t  <jats:p>In our evaluation of the implementation, we find a severe performance degradation when compiling parts of the Coq standard library, inherent to the algorithm itself. We conclude that if we wish to maintain backward compatibility, using size inference as a replacement for syntactic checking is impractical in terms of performance.<\/jats:p>","DOI":"10.1017\/s0956796822000120","type":"journal-article","created":{"date-parts":[[2023,1,24]],"date-time":"2023-01-24T07:30:24Z","timestamp":1674545424000},"update-policy":"https:\/\/doi.org\/10.1017\/policypage","source":"Crossref","is-referenced-by-count":2,"title":["Is sized typing for Coq practical?"],"prefix":"10.1017","volume":"33","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0830-3180","authenticated-orcid":false,"given":"JONATHAN","family":"CHAN","sequence":"first","affiliation":[]},{"given":"YUFENG","family":"LI","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6402-4840","authenticated-orcid":false,"given":"WILLIAM J.","family":"BOWMAN","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2023,1,24]]},"reference":[{"volume-title":"Theses","year":"2006","author":"Abel","key":"S0956796822000120_ref2"},{"key":"S0956796822000120_ref22","doi-asserted-by":"publisher","DOI":"10.1145\/237721.240882"},{"key":"S0956796822000120_ref3","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.43.2"},{"key":"S0956796822000120_ref8","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48167-2_1"},{"key":"S0956796822000120_ref23","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.TYPES.2020.8"},{"key":"S0956796822000120_ref26","unstructured":"Sacchini, J. L. (2011) On type-based termination and dependent pattern matching in the calculus of inductive constructions. Theses. \u00c9cole Nationale Sup\u00e9rieure des Mines de Paris. url: https:\/\/pastel.archives-ouvertes.fr\/pastel-00622429."},{"key":"S0956796822000120_ref6","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796816000022"},{"key":"S0956796822000120_ref12","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129503004122"},{"key":"S0956796822000120_ref17","doi-asserted-by":"crossref","first-page":"87","DOI":"10.1090\/qam\/102435","article-title":"On a routing problem","volume":"16","author":"Ford","year":"1958","journal-title":"Quart. Appl. Math."},{"key":"S0956796822000120_ref18","unstructured":"Frade, M. J. (2004) Type-Based Termination of Recursive Definitions and Constructor Subtyping in Typed Lambda Calculi. PhD Thesis. University of Minho. Braga, Portugal. url: https:\/\/haslab.uminho.pt\/sites\/default\/files\/mjf\/files\/thesis.pdf."},{"key":"S0956796822000120_ref13","doi-asserted-by":"publisher","DOI":"10.1007\/11417170_7"},{"key":"S0956796822000120_ref24","doi-asserted-by":"publisher","DOI":"10.1007\/s11225-013-9470-y"},{"key":"S0956796822000120_ref27","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2013.29"},{"key":"S0956796822000120_ref1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-27836-8_8"},{"key":"S0956796822000120_ref31","unstructured":"Sacchini, J. L. (2015) Well-Founded Sized Types in the Calculus of (Co)Inductive Constructions. Unpublished paper. url: https:\/\/web.archive.org\/web\/20160606143713\/ http:\/\/www.qatar.cmu.edu\/sacchini\/well-founded\/well-founded.pdf."},{"key":"S0956796822000120_ref7","doi-asserted-by":"publisher","DOI":"10.1145\/311027710.1145\/3110277"},{"key":"S0956796822000120_ref19","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-60579-7_3"},{"volume-title":"Lambda Calculi with Types","year":"1993","author":"Barendregt","key":"S0956796822000120_ref10"},{"key":"S0956796822000120_ref20","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0055070"},{"key":"S0956796822000120_ref5","doi-asserted-by":"publisher","DOI":"10.1145\/3158111"},{"key":"S0956796822000120_ref15","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-87531-4_35"},{"key":"S0956796822000120_ref32","unstructured":"Sacchini, J. L. (2016). Coqinline732: Type-Based Termination in the Coq Proof Assistant. url: https:\/\/web.archive.org\/web\/20160530175545\/ http:\/\/www.qatar.cmu.edu\/sacchini\/coq.html."},{"key":"S0956796822000120_ref35","unstructured":"The Coq Development Team. (2018). CoqTerminationDiscussion. url: https:\/\/github.com\/coq\/coq\/wiki\/CoqTerminationDiscussion."},{"key":"S0956796822000120_ref34","doi-asserted-by":"publisher","DOI":"10.1145\/3371076"},{"volume-title":"Difference Constraints and Shortest Paths","year":"2009","author":"Cormen","key":"S0956796822000120_ref16"},{"key":"S0956796822000120_ref4","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.77.1"},{"key":"S0956796822000120_ref11","unstructured":"Barras, B. (2012) Semantical Investigations in Intuitionistic Set Theory and Type Theories with Inductive Families. Habilitation thesis. Universit\u00e9 Paris Diderot (Paris 7). url: http:\/\/www.lsv.fr\/barras\/habilitation\/barras-habilitation.pdf."},{"key":"S0956796822000120_ref37","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.5661975"},{"key":"S0956796822000120_ref30","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.3928999"},{"key":"S0956796822000120_ref14","doi-asserted-by":"publisher","DOI":"10.1007\/11916277_18"},{"key":"S0956796822000120_ref21","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-16242-8_24"},{"key":"S0956796822000120_ref29","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.5182857"},{"key":"S0956796822000120_ref28","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-07151-0_11"},{"key":"S0956796822000120_ref25","first-page":"240","volume-title":"Types for Proofs and Programs","author":"Miquel","year":"2002"},{"key":"S0956796822000120_ref36","unstructured":"The Coq Development Team. (2021) The Coq Proof Assistant (8.13). Zenodo. url: https:\/\/github.com\/coq\/coq\/tree\/V8.13.0."},{"key":"S0956796822000120_ref33","volume-title":"Pure type systems with definitions","volume":"9324","author":"Severi","year":"1993"},{"key":"S0956796822000120_ref9","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0053541"}],"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0956796822000120","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,24]],"date-time":"2023-01-24T07:30:39Z","timestamp":1674545439000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0956796822000120\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"references-count":37,"alternative-id":["S0956796822000120"],"URL":"https:\/\/doi.org\/10.1017\/s0956796822000120","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"type":"print","value":"0956-7968"},{"type":"electronic","value":"1469-7653"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"\u00a9 The Author(s), 2023. Published by Cambridge University Press","name":"copyright","label":"Copyright","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}},{"value":"This is an Open Access article, distributed under the terms of the Creative Commons Attribution licence (https:\/\/creativecommons.org\/licenses\/by\/4.0\/), which permits unrestricted re-use, distribution and reproduction, provided the original article is properly cited.","name":"license","label":"License","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}],"article-number":"e1"}}