{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,26]],"date-time":"2026-09-26T12:30:07Z","timestamp":1790425807191,"version":"4.1.0"},"reference-count":30,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","license":[{"start":{"date-parts":[[2019,7,26]],"date-time":"2019-07-26T00:00:00Z","timestamp":1564099200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2019,7,26]]},"abstract":"<jats:p>Traditional approaches to compensate for the lack of exceptions in type theories for proof assistants have severe drawbacks from both a programming and a reasoning perspective.<\/jats:p>\n          <jats:p>P\u00e9drot and Tabareau recently extended the Calculus of Inductive Constructions (CIC) with exceptions. The new exceptional type theory is interpreted by a translation into CIC, covering full dependent elimination, decidable type-checking and canonicity. However, the exceptional theory is inconsistent as a logical system. To recover consistency, P\u00e9drot and Tabareau propose an additional translation that uses parametricity to enforce that all exceptions are caught locally. While this enforcement brings logical expressivity gains over CIC, it completely prevents reasoning about exceptional programs such as partial functions.<\/jats:p>\n          <jats:p>\n            This work addresses the dilemma between exceptions and consistency in a more flexible manner, with the\n            <jats:italic>Reasonably Exceptional Type Theory<\/jats:italic>\n            (RETT). RETT is structured in three layers: (a) the\n            <jats:italic>exceptional<\/jats:italic>\n            layer, in which all terms can raise exceptions; (b) the\n            <jats:italic>mediation<\/jats:italic>\n            layer, in which exceptional terms must be provably parametric; (c) the\n            <jats:italic>pure<\/jats:italic>\n            layer, in which terms are non-exceptional, but can refer to exceptional terms.\n          <\/jats:p>\n          <jats:p>We present the general theory of RETT, where each layer is realized by a predicative hierarchy of universes, and develop an instance of RETT in Coq: the impure layer corresponds to the predicative universe hierarchy, the pure layer is realized by the impredicative universe of propositions, and the mediation layer is reified via a parametricity type class. RETT is the first full dependent type theory to support consistent reasoning about exceptional terms, and the CoqRETT plugin readily brings this ability to Coq programmers.<\/jats:p>","DOI":"10.1145\/3341712","type":"journal-article","created":{"date-parts":[[2019,7,29]],"date-time":"2019-07-29T20:55:51Z","timestamp":1564433751000},"page":"1-29","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":14,"title":["A reasonably exceptional type theory"],"prefix":"10.1145","volume":"3","author":[{"given":"Pierre-Marie","family":"P\u00e9drot","sequence":"first","affiliation":[{"name":"Inria, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Nicolas","family":"Tabareau","sequence":"additional","affiliation":[{"name":"Inria, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Hans Jacob","family":"Fehrmann","sequence":"additional","affiliation":[{"name":"University of Chile, Chile"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"\u00c9ric","family":"Tanter","sequence":"additional","affiliation":[{"name":"University of Chile, Chile \/ Inria, France"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2019,7,26]]},"reference":[{"key":"e_1_2_2_1_1","volume-title":"Dependent Types and Fibred Computational Effects. In 19th International Conference on Foundations of Software Science and Computation Structures. Springer Berlin Heidelberg","author":"Ahman Danel","unstructured":"Danel Ahman , Neil Ghani , and Gordon D. Plotkin . 2016 . Dependent Types and Fibred Computational Effects. In 19th International Conference on Foundations of Software Science and Computation Structures. Springer Berlin Heidelberg , Eindhoven, The Netherlands, 36\u201354. DOI : Danel Ahman, Neil Ghani, and Gordon D. Plotkin. 2016. Dependent Types and Fibred Computational Effects. In 19th International Conference on Foundations of Software Science and Computation Structures. Springer Berlin Heidelberg, Eindhoven, The Netherlands, 36\u201354. DOI:"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1010000206149"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.5555\/1987171.1987181"},{"key":"e_1_2_2_4_1","doi-asserted-by":"crossref","unstructured":"Yves Bertot and Pierre Cast\u00e9ran. 2004. Interactive Theorem Proving and Program Development.   Yves Bertot and Pierre Cast\u00e9ran. 2004. Interactive Theorem Proving and Program Development.","DOI":"10.1007\/978-3-662-07964-5"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3018610.3018620"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158110"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1017\/S095679681300018X"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236784"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535883"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1596550.1596565"},{"key":"e_1_2_2_11_1","volume-title":"Sprinkles of Extensionality for Your Vanilla Type Theory. In 22nd International Conference on Types for Proofs and Programs (TYPES","author":"Cockx Jesper","year":"2016","unstructured":"Jesper Cockx and Andreas Abel . 2016 . Sprinkles of Extensionality for Your Vanilla Type Theory. In 22nd International Conference on Types for Proofs and Programs (TYPES 2016). Jesper Cockx and Andreas Abel. 2016. Sprinkles of Extensionality for Your Vanilla Type Theory. In 22nd International Conference on Types for Proofs and Programs (TYPES 2016)."},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(88)90005-3"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2935320"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535841"},{"key":"e_1_2_2_15_1","volume-title":"ERTS 2016: Embedded Real Time Software and Systems. SEE.","author":"Leroy Xavier","year":"2016","unstructured":"Xavier Leroy , Sandrine Blazy , Daniel K\u00e4stner , Bernhard Schommer , Markus Pister , and Christian Ferdinand . 2016 . CompCert \u2013 A Formally Verified Optimizing Compiler . In ERTS 2016: Embedded Real Time Software and Systems. SEE. Xavier Leroy, Sandrine Blazy, Daniel K\u00e4stner, Bernhard Schommer, Markus Pister, and Christian Ferdinand. 2016. CompCert \u2013 A Formally Verified Optimizing Compiler. In ERTS 2016: Embedded Real Time Software and Systems. SEE."},{"key":"e_1_2_2_17_1","unstructured":"Paul Blain Levy. 2001. Call-by-push-value. Ph.D. Dissertation. Queen Mary University of London.  Paul Blain Levy. 2001. Call-by-push-value. Ph.D. Dissertation. Queen Mary University of London."},{"key":"e_1_2_2_18_1","unstructured":"Assia Mahboubi and Enrico Tassi. 2008. Mathematical Components.  Assia Mahboubi and Enrico Tassi. 2008. Mathematical Components."},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90052-4"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796808006953"},{"key":"e_1_2_2_21_1","volume-title":"Advanced Functional Programming (AFP 2008) (LNCS)","author":"Norell Ulf","unstructured":"Ulf Norell . 2009. Dependently Typed Programming in Agda . In Advanced Functional Programming (AFP 2008) (LNCS) , Vol. 5832 . Springer , 230\u2013266. Ulf Norell. 2009. Dependently Typed Programming in Agda. In Advanced Functional Programming (AFP 2008) (LNCS), Vol. 5832. Springer, 230\u2013266."},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.5555\/3329995.3330048"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89884-1_9"},{"key":"e_1_2_2_24_1","unstructured":"The Coq Development Team. 2019. The Coq Proof Assistant Reference Manual. (2019). https:\/\/coq.inria.fr\/refman  The Coq Development Team. 2019. The Coq Proof Assistant Reference Manual. (2019). https:\/\/coq.inria.fr\/refman"},{"key":"e_1_2_2_25_1","volume-title":"IFIP Congress (2002-01-03)","author":"Reynolds John C.","year":"1983","unstructured":"John C. Reynolds . 1983 . Types, Abstraction and Parametric Polymorphism .. In IFIP Congress (2002-01-03) . 513\u2013523. John C. Reynolds. 1983. Types, Abstraction and Parametric Polymorphism.. In IFIP Congress (2002-01-03). 513\u2013523."},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71067-7_23"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837655"},{"key":"e_1_2_2_28_1","unstructured":"Univalent Foundations Project. 2013. Homotopy Type Theory: Univalent Foundations for Mathematics. http:\/\/ homotopytypetheory.org\/book .  Univalent Foundations Project. 2013. Homotopy Type Theory: Univalent Foundations for Mathematics. http:\/\/ homotopytypetheory.org\/book ."},{"key":"e_1_2_2_29_1","unstructured":"Matthijs V\u00e1k\u00e1r. 2015. A Framework for Dependent Types and Effects. (2015). arXiv: arXiv:1512.08009 draft.  Matthijs V\u00e1k\u00e1r. 2015. A Framework for Dependent Types and Effects. (2015). arXiv: arXiv:1512.08009 draft."},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.5555\/2952803.2953003"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/292540.292560"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3341712","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3341712","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T00:43:24Z","timestamp":1750207404000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3341712"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,7,26]]},"references-count":30,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2019,7,26]]}},"alternative-id":["10.1145\/3341712"],"URL":"https:\/\/doi.org\/10.1145\/3341712","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,7,26]]},"assertion":[{"value":"2019-07-26","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}