{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T10:07:39Z","timestamp":1770286059911,"version":"3.49.0"},"reference-count":35,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","license":[{"start":{"date-parts":[[2022,8,29]],"date-time":"2022-08-29T00:00:00Z","timestamp":1661731200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"CONICYT FONDECYT","award":["1190058"],"award-info":[{"award-number":["1190058"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2022,8,29]]},"abstract":"<jats:p>\n            Gradual dependent types can help with the incremental adoption of dependently typed code by providing a principled semantics for\n            <jats:italic>imprecise<\/jats:italic>\n            types and proofs, where some parts have been omitted. Current theories of gradual dependent types, though, lack a central feature of type theory: propositional equality. Lennon-Bertrand et al. show that, when the reflexive proof\n            <jats:italic>refl<\/jats:italic>\n            is the only closed value of an equality type, a gradual extension of the Calculus of Inductive Constructions (CIC) with propositional equality violates static observational equivalences. Extensionally-equal functions should be indistinguishable at run time, but they can be distinguished using a combination of equality and type imprecision.\n          <\/jats:p>\n          <jats:p>\n            This work presents a gradual dependently typed language that supports propositional equality. We avoid the above issues by devising an equality type of which\n            <jats:italic>refl<\/jats:italic>\n            is not the only closed inhabitant. Instead, each equality proof is accompanied by a term that is at least as precise as the equated terms, acting as a witness of their plausible equality. These witnesses track partial type information as a program runs, raising errors when that information shows that two equated terms are undeniably inconsistent. Composition of type information is internalized as a construct of the language, and is deferred for function bodies whose evaluation is blocked by variables. We thus ensure that extensionally-equal functions compose without error, thereby preventing contexts from distinguishing them. We describe the challenges of designing consistency and precision relations for this system, along with solutions to these challenges. Finally, we prove important metatheory: type safety, conservative embedding of CIC, weak canonicity, and the gradual guarantees of Siek et al., which ensure that reducing a program\u2019s precision introduces no new static or dynamic errors.\n          <\/jats:p>","DOI":"10.1145\/3547627","type":"journal-article","created":{"date-parts":[[2022,8,31]],"date-time":"2022-08-31T19:39:26Z","timestamp":1661974766000},"page":"165-193","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":6,"title":["Propositional equality for gradual dependently typed programming"],"prefix":"10.1145","volume":"6","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-9631-4826","authenticated-orcid":false,"given":"Joseph","family":"Eremondi","sequence":"first","affiliation":[{"name":"University of British Columbia, Canada"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0982-1118","authenticated-orcid":false,"given":"Ronald","family":"Garcia","sequence":"additional","affiliation":[{"name":"University of British Columbia, Canada"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7359-890X","authenticated-orcid":false,"given":"\u00c9ric","family":"Tanter","sequence":"additional","affiliation":[{"name":"University of Chile, Chile"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2022,8,31]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/1292597.1292608"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434342"},{"key":"e_1_2_1_3_1","unstructured":"Edwin Brady. 2017. Type-driven development with Idris. Manning. isbn:9781617293023 https:\/\/www.manning.com\/books\/type-driven-development-with-idris \t\t\t\t  Edwin Brady. 2017. Type-driven development with Idris. Manning. isbn:9781617293023 https:\/\/www.manning.com\/books\/type-driven-development-with-idris"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951933"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000011"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341692"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/581478.581484"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837670"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/11780274_27"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1093\/oso\/9780198501275.003.0008"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434288"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009856"},{"key":"e_1_2_1_14_1","volume-title":"A Dependently Typed Programming Language With Dynamic Equality. Ph. D. Dissertation","author":"Lemay Mark","unstructured":"Mark Lemay . 2022. A Dependently Typed Programming Language With Dynamic Equality. Ph. D. Dissertation . Boston University . https:\/\/github.com\/marklemay\/thesis Mark Lemay. 2022. A Dependently Typed Programming Language With Dynamic Equality. Ph. D. Dissertation. Boston University. https:\/\/github.com\/marklemay\/thesis"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ITP.2021.24"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3495528"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3547655"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)70727-4"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(09)70189-2"},{"key":"e_1_2_1_20_1","volume-title":"Dependently typed functional programs and their proofs. Ph. D. Dissertation","author":"McBride Conor","year":"1842","unstructured":"Conor McBride . 2000. Dependently typed functional programs and their proofs. Ph. D. Dissertation . University of Edinburgh , UK. http:\/\/hdl.handle.net\/ 1842 \/374 Conor McBride. 2000. Dependently typed functional programs and their proofs. Ph. D. Dissertation. University of Edinburgh, UK. http:\/\/hdl.handle.net\/1842\/374"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45842-5_13"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236768"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103776.2103779"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/1-4020-8141-3_34"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498693"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737968"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796821000241"},{"key":"e_1_2_1_28_1","volume-title":"Gradual Typing for Functional Languages. In Scheme and Functional Programming Workshop. 81\u201392","author":"Jeremy","year":"2006","unstructured":"Jeremy G. Siek and Walid Taha. 2006 . Gradual Typing for Functional Languages. In Scheme and Functional Programming Workshop. 81\u201392 . http:\/\/scheme 2006 .cs.uchicago.edu\/scheme2006.pdf Jeremy G. Siek and Walid Taha. 2006. Gradual Typing for Functional Languages. In Scheme and Functional Programming Workshop. 81\u201392. http:\/\/scheme2006.cs.uchicago.edu\/scheme2006.pdf"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.SNAPL.2015.274"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706342"},{"key":"e_1_2_1_31_1","unstructured":"Thomas Streicher. 1993. Investigations into intensional type theory. Ph. D. Dissertation. Ludwig Maximilian Universit\u00e4t. https:\/\/www2.mathematik.tu-darmstadt.de\/~streicher\/HabilStreicher.pdf Habilitation thesis \t\t\t\t  Thomas Streicher. 1993. Investigations into intensional type theory. Ph. D. Dissertation. Ludwig Maximilian Universit\u00e4t. https:\/\/www2.mathematik.tu-darmstadt.de\/~streicher\/HabilStreicher.pdf Habilitation thesis"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1995.1057"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/2816707.2816710"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00590-9_1"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1093"},{"key":"e_1_2_1_36_1","volume-title":"WGT 2020 ; Conference date: 19-01-2020 Through 25-01-2020","author":"Zalewski Jakub","year":"2020","unstructured":"Jakub Zalewski , James McKinna , J. Garrett Morris , and Philip Wadler . 2020 . \u03bb dB: Blame tracking at higher fidelity. https:\/\/wgt20.irif.fr\/wgt20-final98-acmpaginated.pdf First ACM SIGPLAN Workshop on Gradual Typing 2020 , WGT 2020 ; Conference date: 19-01-2020 Through 25-01-2020 Jakub Zalewski, James McKinna, J. Garrett Morris, and Philip Wadler. 2020. \u03bb dB: Blame tracking at higher fidelity. https:\/\/wgt20.irif.fr\/wgt20-final98-acmpaginated.pdf First ACM SIGPLAN Workshop on Gradual Typing 2020, WGT 2020 ; Conference date: 19-01-2020 Through 25-01-2020"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3547627","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3547627","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T18:43:29Z","timestamp":1750272209000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3547627"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,8,29]]},"references-count":35,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2022,8,29]]}},"alternative-id":["10.1145\/3547627"],"URL":"https:\/\/doi.org\/10.1145\/3547627","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,8,29]]},"assertion":[{"value":"2022-08-31","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}