{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,11]],"date-time":"2026-07-11T18:40:20Z","timestamp":1783795220972,"version":"3.55.0"},"reference-count":21,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2019,1,2]],"date-time":"2019-01-02T00:00:00Z","timestamp":1546387200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-nc-sa\/4.0\/"}],"funder":[{"DOI":"10.13039\/100010663","name":"European Research Council","doi-asserted-by":"publisher","award":["64399"],"award-info":[{"award-number":["64399"]}],"id":[{"id":"10.13039\/100010663","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":[[2019,1,2]]},"abstract":"<jats:p>Definitional equality\u2014or conversion\u2014for a type theory with a decidable type checking is the simplest tool to prove that two objects are the same, letting the system decide just using computation. Therefore, the more things are equal by conversion, the simpler it is to use a language based on type theory. Proof-irrelevance, stating that any two proofs of the same proposition are equal, is a possible way to extend conversion to make a type theory more powerful. However, this new power comes at a price if we integrate it naively, either by making type checking undecidable or by realizing new axioms\u2014such as uniqueness of identity proofs (UIP)\u2014that are incompatible with other extensions, such as univalence. In this paper, taking inspiration from homotopy type theory, we propose a general way to extend a type theory with definitional proof irrelevance, in a way that keeps type checking decidable and is compatible with univalence. We provide a new criterion to decide whether a proposition can be eliminated over a type (correcting and improving the so-called singleton elimination of Coq) by using techniques coming from recent development on dependent pattern matching without UIP. We show the generality of our approach by providing implementations for both Coq and Agda, both of which are planned to be integrated in future versions of those proof assistants.<\/jats:p>","DOI":"10.1145\/3290316","type":"journal-article","created":{"date-parts":[[2019,1,4]],"date-time":"2019-01-04T13:33:51Z","timestamp":1546608831000},"page":"1-28","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":42,"title":["Definitional proof-irrelevance without K"],"prefix":"10.1145","volume":"3","author":[{"given":"Ga\u00ebtan","family":"Gilbert","sequence":"first","affiliation":[{"name":"Inria, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jesper","family":"Cockx","sequence":"additional","affiliation":[{"name":"Chalmers University of Technology, Sweden \/ University of Gothenburg, Sweden"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Matthieu","family":"Sozeau","sequence":"additional","affiliation":[{"name":"Inria, France \/ IRIF, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Nicolas","family":"Tabareau","sequence":"additional","affiliation":[{"name":"Inria, France"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2019,1,2]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158111"},{"key":"e_1_2_2_2_1","volume-title":"On Irrelevance and Algorithmic Equality in Predicative Type Theory. Logical Methods in Computer Science 8, 1 (03","author":"Abel Andreas","year":"2012"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.5555\/788021.788977"},{"key":"e_1_2_2_4_1","unstructured":"Thorsten Altenkirch Paolo Capriotti and Nicolai Kraus. 2016. Extending Homotopy Type Theory with Strict Equality. In CSL.  Thorsten Altenkirch Paolo Capriotti and Nicolai Kraus. 2016. Extending Homotopy Type Theory with Strict Equality. In CSL."},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/14.4.447"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3018610.3018620"},{"key":"e_1_2_2_7_1","volume-title":"Types for Proofs and Programs","author":"Brady Edwin"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236770"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1017\/S095679681800014X"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2692915.2628139"},{"key":"e_1_2_2_12_1","unstructured":"Thierry Coquand. 2016. Universe of Bishop sets. (2016). www.cse.chalmers.se\/~coquand\/bishop.pdf .  Thierry Coquand. 2016. Universe of Bishop sets. (2016). www.cse.chalmers.se\/~coquand\/bishop.pdf ."},{"key":"e_1_2_2_13_1","doi-asserted-by":"crossref","volume-title":"Types for Proofs and Programs","author":"Dybjer Peter","DOI":"10.1007\/3-540-60579-7"},{"key":"e_1_2_2_14_1","volume-title":"International Workshop on Types for Proofs and Programs. Springer, 153\u2013164","author":"Hofmann Martin","year":"1995"},{"key":"e_1_2_2_16_1","unstructured":"Cyprien Mangin and Matthieu Sozeau. 2018. Equations Reloaded. (2018). http:\/\/mattam82.github.io\/Coq-Equations\/  Cyprien Mangin and Matthieu Sozeau. 2018. Equations Reloaded. (2018). http:\/\/mattam82.github.io\/Coq-Equations\/"},{"key":"e_1_2_2_17_1","volume-title":"Logic Colloquium \u201973","author":"Martin-L\u00f6f Per"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.5555\/871816.871845"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2018.03.002"},{"key":"e_1_2_2_20_1","volume-title":"Homotopy Type Theory: Univalent Foundations of Mathematics","author":"Foundations Program The Univalent"},{"key":"e_1_2_2_21_1","unstructured":"Vladimir Voevodsky. 2011. Resising Rules - their use and semantic justification. www.math.ias.edu\/~vladimir\/Site3\/ Univalent_Foundations_files\/2011_Bergen.pdf . (2011).  Vladimir Voevodsky. 2011. Resising Rules - their use and semantic justification. www.math.ias.edu\/~vladimir\/Site3\/ Univalent_Foundations_files\/2011_Bergen.pdf . (2011)."},{"key":"e_1_2_2_22_1","unstructured":"Vladimir Voevodsky. 2013. A simple type system with two identity types. (2013). https:\/\/ncatlab.org\/homotopytypetheory\/ files\/HTS.pdf  Vladimir Voevodsky. 2013. A simple type system with two identity types. (2013). https:\/\/ncatlab.org\/homotopytypetheory\/ files\/HTS.pdf"},{"key":"e_1_2_2_23_1","volume-title":"On the Strength of Proof-Irrelevant Type Theories. 4 (09","author":"Werner Benjamin","year":"2008"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3290316","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3290316","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T01:02:07Z","timestamp":1750208527000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3290316"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,1,2]]},"references-count":21,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2019,1,2]]}},"alternative-id":["10.1145\/3290316"],"URL":"https:\/\/doi.org\/10.1145\/3290316","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,1,2]]},"assertion":[{"value":"2019-01-02","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}