{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,2]],"date-time":"2026-10-02T07:53:19Z","timestamp":1790927599352,"version":"4.1.0"},"reference-count":46,"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":[{"DOI":"10.13039\/501100001665","name":"Agence Nationale de la Recherche","doi-asserted-by":"publisher","award":["ProverFX - ANR-21-ERCC-0004"],"award-info":[{"award-number":["ProverFX - ANR-21-ERCC-0004"]}],"id":[{"id":"10.13039\/501100001665","id-type":"DOI","asserted-by":"publisher"}]}],"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>Gradualizing the Calculus of Inductive Constructions (CIC) involves dealing with subtle tensions between normalization, graduality, and conservativity with respect to CIC. Recently, GCIC has been proposed as a parametrized gradual type theory that admits three variants, each sacrificing one of these properties. For devising a gradual proof assistant based on CIC, normalization and conservativity with respect to CIC are key, but the tension with graduality needs to be addressed. Additionally, several challenges remain:  \n(1) The presence of two wildcard terms at any type---the error and unknown terms---enables trivial proofs of any theorem, jeopardizing the use of a gradual type theory in a proof assistant;  \n(2) Supporting general indexed inductive families, most prominently equality, is an open problem;  \n(3) Theoretical accounts of gradual typing and graduality so far do not support handling type mismatches detected during reduction;  \n(4) Precision and graduality are external notions not amenable to reasoning within a gradual type theory.  \nAll these issues manifest primally in CastCIC, the cast calculus used to define GCIC. In this work, we present an extension of CastCIC called GRIP. GRIP is a reasonably gradual type theory that addresses the issues above, featuring internal precision and general exception handling. By adopting a novel interpretation of the unknown term that carefully accounts for universe levels, GRIP satisfies graduality for a large and well-defined class of terms, in addition to being normalizing and a conservative extension of CIC. Internal precision supports reasoning about graduality within GRIP itself, for instance to characterize gradual exception-handling terms, and supports gradual subset types. We develop the metatheory of GRIP using a model formalized in Coq, and provide a prototype implementation of GRIP in Agda.<\/jats:p>","DOI":"10.1145\/3547655","type":"journal-article","created":{"date-parts":[[2022,8,31]],"date-time":"2022-08-31T19:39:26Z","timestamp":1661974766000},"page":"931-959","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":12,"title":["A reasonably gradual type theory"],"prefix":"10.1145","volume":"6","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-5554-3203","authenticated-orcid":false,"given":"Kenji","family":"Maillard","sequence":"first","affiliation":[{"name":"Inria, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7079-8826","authenticated-orcid":false,"given":"Meven","family":"Lennon-Bertrand","sequence":"additional","affiliation":[{"name":"Inria, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3366-2273","authenticated-orcid":false,"given":"Nicolas","family":"Tabareau","sequence":"additional","affiliation":[{"name":"Inria, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7359-890X","authenticated-orcid":false,"given":"\u00c9ric","family":"Tanter","sequence":"additional","affiliation":[{"name":"University of Chile, Chile"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2022,8,31]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-8(1:29)2012"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1017\/S095679681500009X"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/1292597.1292608"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796812000056"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3018610.3018620"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535883"},{"key":"e_1_2_1_8_1","first-page":"3127","article-title":"Cubical Type Theory","volume":"4","author":"Cohen Cyril","year":"2017","unstructured":"Cyril Cohen , Thierry Coquand , Simon Huber , and Anders M\u00f6rtberg . 2017 . Cubical Type Theory : A Constructive Interpretation of the Univalence Axiom. FLAP , 4 , 10 (2017), 3127 \u2013 3170 . http:\/\/collegepublications.co.uk\/ifcolog\/?00019 Cyril Cohen, Thierry Coquand, Simon Huber, and Anders M\u00f6rtberg. 2017. Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom. FLAP, 4, 10 (2017), 3127\u20133170. http:\/\/collegepublications.co.uk\/ifcolog\/?00019","journal-title":"A Constructive Interpretation of the Univalence Axiom. FLAP"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000011"},{"key":"e_1_2_1_10_1","unstructured":"Richard A. Eisenberg. 2016. Dependent Types in Haskell: Theory and Practice. arxiv:1610.07978. \t\t\t\t  Richard A. Eisenberg. 2016. Dependent Types in Haskell: Theory and Practice. arxiv:1610.07978."},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3547627"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341692"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290316"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3373718"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.TYPES.2020.8"},{"key":"e_1_2_1_17_1","volume-title":"Proceedings of the 24th ACM SIGPLAN Conference on Functional Programming (ICFP","year":"2019","unstructured":"2019. Proceedings of the 24th ACM SIGPLAN Conference on Functional Programming (ICFP 2019 ). 3, ACM Press. 2019. Proceedings of the 24th ACM SIGPLAN Conference on Functional Programming (ICFP 2019). 3, ACM Press."},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103776.2103780"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111059"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1090\/pspum\/017\/0257175"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009856"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3495528"},{"key":"e_1_2_1_23_1","unstructured":"Per Martin-L\u00f6f. 1971. An Intuitionistic Theory of Types. Unpublished manuscript. \t\t\t\t  Per Martin-L\u00f6f. 1971. An Intuitionistic Theory of Types. Unpublished manuscript."},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236768"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103776.2103779"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/1-4020-8141-3_34"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2017.8005113"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89884-1_9"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371126"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341712"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498693"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.21136\/HS.2017.06"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375602"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3373718.3394759"},{"key":"e_1_2_1_35_1","volume-title":"Proceedings of the Scheme and Functional Programming Workshop. 81\u201392","author":"Siek Jeremy","year":"2006","unstructured":"Jeremy Siek and Walid Taha . 2006 . Gradual Typing for Functional Languages . In Proceedings of the Scheme and Functional Programming Workshop. 81\u201392 . Jeremy Siek and Walid Taha. 2006. Gradual Typing for Functional Languages. In Proceedings of the Scheme and Functional Programming Workshop. 81\u201392."},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706342"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.SNAPL.2015.274"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.29007\/3w36"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1995.1057"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/2816707.2816710"},{"key":"e_1_2_1_42_1","unstructured":"The Coq Development Team. 2020. The Coq proof assistant reference manual. https:\/\/coq.inria.fr\/refman\/ Version 8.12. \t\t\t\t  The Coq Development Team. 2020. The Coq proof assistant reference manual. https:\/\/coq.inria.fr\/refman\/ Version 8.12."},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341691"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00590-9_1"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/3373718.3394794"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/277650.277732"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3547655","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3547655","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\/3547655"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,8,29]]},"references-count":46,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2022,8,29]]}},"alternative-id":["10.1145\/3547655"],"URL":"https:\/\/doi.org\/10.1145\/3547655","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"}}]}}