{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,9]],"date-time":"2025-12-09T11:55:04Z","timestamp":1765281304209,"version":"3.46.0"},"reference-count":54,"publisher":"Cambridge University Press (CUP)","license":[{"start":{"date-parts":[[2025,12,9]],"date-time":"2025-12-09T00:00:00Z","timestamp":1765238400000},"content-version":"unspecified","delay-in-days":342,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["cambridge.org"],"crossmark-restriction":true},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    We present a new way to control the unfolding of definitions in dependent type theory. Traditionally, proof assistants require users to fix whether each definition will or will not be unfolded in the remainder of a development; unfolding definitions is often necessary in order to reason about them, but an excess of unfolding can result in brittle proofs and intractably large proof goals. In our system, definitions are by default not unfolded, but users can selectively unfold them in a local manner. We justify our mechanism by means of elaboration to a core theory with\n                    <jats:italic>extension types \u2013<\/jats:italic>\n                    a connective first introduced in the context of homotopy type theory \u2013 and by establishing a normalization theorem for our core calculus. We have implemented controlled unfolding in the\n                    <jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"png\" xlink:href=\"S0960129525100327_inline1.png\"\/>\n                    proof assistant, inspiring an independent implementation in Agda.\n                  <\/jats:p>","DOI":"10.1017\/s0960129525100327","type":"journal-article","created":{"date-parts":[[2025,12,9]],"date-time":"2025-12-09T11:23:53Z","timestamp":1765279433000},"update-policy":"https:\/\/doi.org\/10.1017\/policypage","source":"Crossref","is-referenced-by-count":0,"title":["Controlling unfolding in type theory"],"prefix":"10.1017","volume":"35","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-1944-0789","authenticated-orcid":false,"given":"Daniel","family":"Gratzer","sequence":"first","affiliation":[{"id":[{"id":"https:\/\/ror.org\/01aj84f44","id-type":"ROR","asserted-by":"publisher"}],"name":"Aarhus University"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0585-5564","authenticated-orcid":false,"given":"Jonathan","family":"Sterling","sequence":"additional","affiliation":[{"name":"University of Cambridge"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9590-3303","authenticated-orcid":false,"given":"Carlo","family":"Angiuli","sequence":"additional","affiliation":[{"name":"Indiana University"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5429-5153","authenticated-orcid":false,"given":"Thierry","family":"Coquand","sequence":"additional","affiliation":[{"name":"University of Gothenburg"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lars","family":"Birkedal","sequence":"additional","affiliation":[{"id":[{"id":"https:\/\/ror.org\/01aj84f44","id-type":"ROR","asserted-by":"publisher"}],"name":"Aarhus University"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2025,12,9]]},"reference":[{"key":"S0960129525100327_ref25","article-title":"Featherweight veriFast","volume":"11","author":"Jacobs","year":"2015","journal-title":"Logical Methods in Computer Science"},{"key":"S0960129525100327_ref23","unstructured":"Hou (Favonia), K.-B. (2022). kado. http:\/\/www.github.com\/RedPRL\/kado."},{"key":"S0960129525100327_ref3","first-page":"6:1","volume-title":"27th EACSL Annual Conference on Computer Science Logic (CSL 2018) Dagstuhl, Germany","volume":"119","author":"Angiuli","year":"2018"},{"key":"S0960129525100327_ref7","unstructured":"Cartmell, J. (1978). Generalised Algebraic Theories and Contextual Categories. Phd thesis, University of Oxford."},{"key":"S0960129525100327_ref9","first-page":"3127","article-title":"Cubical type theory: a constructive interpretation of the univalence axiom","volume":"4","author":"Cohen","year":"2017","journal-title":"IfCoLog Journal of Logics and Their Applications"},{"key":"S0960129525100327_ref22","doi-asserted-by":"publisher","DOI":"10.7551\/mitpress\/5641.003.0019"},{"key":"S0960129525100327_ref47","unstructured":"The Agda Development Team (2023). Consider where we can use opaque mechanism to provide abstraction. https:\/\/github.com\/agda\/agda-stdlib\/issues\/2136."},{"key":"S0960129525100327_ref44","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39038-8_6"},{"key":"S0960129525100327_ref15","unstructured":"Fiore, M. P. (2022). Semantic analysis of normalisation by evaluation for typed lambda calculus. Unpublished extended version of PPDP \u201902 paper with same title, available at https:\/\/arxiv.org\/abs\/2207.08777."},{"key":"S0960129525100327_ref17","doi-asserted-by":"publisher","DOI":"10.1145\/3290316"},{"key":"S0960129525100327_ref39","unstructured":"Sterling, J. (2021). First Steps in Synthetic Tait Computability: The Objective Metatheory of Cubical Type Theory. Phd thesis, Carnegie Mellon University. Version 1.1, revised May 2022."},{"key":"S0960129525100327_ref27","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0037110"},{"key":"S0960129525100327_ref50","unstructured":"The 1Lab Development Team (2022). The 1Lab. https:\/\/1lab.dev."},{"key":"S0960129525100327_ref54","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4020-5587-4_8"},{"key":"S0960129525100327_ref11","unstructured":"Dagand, P.-E. (2013). A Cosmology of Datatypes: Reusability and Dependent Types. Phd thesis, University of Strathclyde, Glasgow, Scotland."},{"key":"S0960129525100327_ref29","unstructured":"Kov\u00e1cs, A. (2023). smalltt."},{"key":"S0960129525100327_ref52","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129523000208"},{"key":"S0960129525100327_ref8","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129513000881"},{"key":"S0960129525100327_ref21","doi-asserted-by":"publisher","DOI":"10.1145\/3341711"},{"key":"S0960129525100327_ref1","doi-asserted-by":"publisher","DOI":"10.1017\/9781108854429.007"},{"key":"S0960129525100327_ref2","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129521000347"},{"key":"S0960129525100327_ref10","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(95)00021-6"},{"key":"S0960129525100327_ref4","first-page":"1","volume-title":"Computer Science Logic","author":"Aspinall","year":"1995"},{"key":"S0960129525100327_ref13","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-61780-9_66"},{"key":"S0960129525100327_ref14","first-page":"26","volume-title":"Proceedings of the 4th ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming, PPDP\u201902","author":"Fiore","year":"2002"},{"key":"S0960129525100327_ref30","unstructured":"Kov\u00e1cs, A. (2024). Efficient elaboration with controlled definition unfolding. In: Third Workshop on the Implementation of Type Systems."},{"key":"S0960129525100327_ref34","doi-asserted-by":"publisher","DOI":"10.7551\/mitpress\/2319.001.0001"},{"key":"S0960129525100327_ref33","doi-asserted-by":"crossref","unstructured":"Martin-L\u00f6f, P. (1975). An intuitionistic theory of types: predicative part. In: Rose, H. and Shepherdson, J. (eds.) Logic Colloquium\u201973, Proceedings of the Logic Colloquium, Studies in Logic and the Foundations of Mathematics, vol. 80, North-Holland, 73\u2013118.","DOI":"10.1016\/S0049-237X(08)71945-1"},{"key":"S0960129525100327_ref40","first-page":"391","volume-title":"Toward a Geometry for Syntax","author":"Sterling","year":"2025"},{"key":"S0960129525100327_ref43","doi-asserted-by":"publisher","DOI":"10.1145\/1183278.1183281"},{"key":"S0960129525100327_ref42","doi-asserted-by":"publisher","DOI":"10.1145\/3474834"},{"key":"S0960129525100327_ref20","unstructured":"Gratzer, D. and Sterling, J. (2020). Syntactic categories for dependent type theory: sketching and adequacy. Unpublished manuscript. https:\/\/arxiv.org\/abs\/2012.10783."},{"key":"S0960129525100327_ref49","unstructured":"The Coq Development Team (2022). The Coq proof assistant."},{"key":"S0960129525100327_ref35","unstructured":"Newstead, C. (2018). Algebraic Models of Dependent Type Theory. Phd thesis, Carnegie Mellon University."},{"key":"S0960129525100327_ref41","doi-asserted-by":"crossref","unstructured":"Sterling, J. and Angiuli, C. (2021). Normalization for cubical type theory. In: Proceedings of the 36th Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS\u201921, New York, NY, USA, ACM.","DOI":"10.1109\/LICS52264.2021.9470719"},{"key":"S0960129525100327_ref6","unstructured":"Bocquet, R. , Kaposi, A. and Sattler, C. (2021). Relative induction principles for type theories. Unpublished manuscript. https:\/\/arxiv.org\/abs\/2102.11649."},{"key":"S0960129525100327_ref37","unstructured":"RedPRL Development Team, T. (2020). cooltt. http:\/\/www.github.com\/RedPRL\/cooltt."},{"key":"S0960129525100327_ref51","unstructured":"Uemura, T. (2021). Abstract and Concrete Type Theories. Phd thesis, Institute for Logic, Language and Computation, University of Amsterdam."},{"key":"S0960129525100327_ref32","unstructured":"Liao, A. and Cockx, J. (2022). Unfolding control for abstract blocks. https:\/\/github.com\/agda\/agda\/pull\/6354."},{"key":"S0960129525100327_ref12","first-page":"236","volume-title":"Proceedings of the 30th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL\u201903, New Orleans, Louisiana, USA","author":"Dreyer","year":"2003"},{"key":"S0960129525100327_ref16","doi-asserted-by":"publisher","DOI":"10.1017\/S0004972700044828"},{"key":"S0960129525100327_ref5","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129516000268"},{"key":"S0960129525100327_ref38","doi-asserted-by":"publisher","DOI":"10.21136\/HS.2017.06"},{"key":"S0960129525100327_ref46","unstructured":"The Agda Development Team (2022). The Agda standard library. https:\/\/github.com\/agda\/agda-stdlib."},{"key":"S0960129525100327_ref53","volume-title":"Homotopy Type Theory: Univalent Foundations of Mathematics","year":"2013"},{"key":"S0960129525100327_ref18","unstructured":"Gonthier, G. , Mahboubi, A. and Tassi, E. (2016). A small scale reflection extension for the Coq system. Research Report RR-6455, Inria Saclay Ile de France."},{"key":"S0960129525100327_ref26","volume-title":"Topos Theory","author":"Johnstone","year":"1977"},{"key":"S0960129525100327_ref28","doi-asserted-by":"publisher","DOI":"10.1145\/3290315"},{"key":"S0960129525100327_ref45","unstructured":"The Agda Community (2023). The Cubical Agda library. https:\/\/github.com\/agda\/cubical\/."},{"key":"S0960129525100327_ref48","unstructured":"The Agda Team (2021). Agda User Manual, Release 2.6.2."},{"key":"S0960129525100327_ref19","unstructured":"Gratzer, D. , Shulman, M. and Sterling, J. (2022). Strict universes for Grothendieck topoi. Unpublished manuscript. https:\/\/arxiv.org\/abs\/2202.12012."},{"key":"S0960129525100327_ref31","volume-title":"A. 2-Categories Companion, 105-191","author":"Lack","year":"2009"},{"key":"S0960129525100327_ref36","doi-asserted-by":"publisher","DOI":"10.1145\/345099.345100"},{"key":"S0960129525100327_ref24","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-018-9469-1"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129525100327","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,12,9]],"date-time":"2025-12-09T11:24:03Z","timestamp":1765279443000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129525100327\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"references-count":54,"alternative-id":["S0960129525100327"],"URL":"https:\/\/doi.org\/10.1017\/s0960129525100327","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"\u00a9 The Author(s), 2025. 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":"e38"}}