{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T22:58:38Z","timestamp":1770245918597,"version":"3.49.0"},"reference-count":45,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2025,1,7]],"date-time":"2025-01-07T00:00:00Z","timestamp":1736208000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["2006535,2327738"],"award-info":[{"award-number":["2006535,2327738"]}],"id":[{"id":"10.13039\/100000001","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":[[2025,1,7]]},"abstract":"<jats:p>The Dependent Calculus of Indistinguishability (DCOI) uses dependency tracking to identify irrelevant arguments and uses indistinguishability during type conversion to enable proof irrelevance, supporting run-time and compile-time irrelevance with the same uniform mechanism. DCOI also internalizes reasoning about indistinguishability through the use of a propositional equality type indexed by an observer level.<\/jats:p>\n                  <jats:p>\n                    As DCOI is a pure type system, prior work establishes only its syntactic type safety, justifying its use as the basis for a programming language with dependent types. However, it was not clear whether any instance of this system would be suitable for use as a type theory for theorem proving. Here, we identify a suitable instance\n                    <jats:inline-formula>\n                      <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\">\n                        <mml:mrow>\n                          <mml:msup>\n                            <mml:mrow>\n                              <mml:mtext>DCOI<\/mml:mtext>\n                            <\/mml:mrow>\n                            <mml:mi>\u03c9<\/mml:mi>\n                          <\/mml:msup>\n                        <\/mml:mrow>\n                      <\/mml:math>\n                    <\/jats:inline-formula>\n                    , which has an infinite predicative universe hierarchy. We show that\n                    <jats:inline-formula>\n                      <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\">\n                        <mml:mrow>\n                          <mml:msup>\n                            <mml:mrow>\n                              <mml:mtext>DCOI<\/mml:mtext>\n                            <\/mml:mrow>\n                            <mml:mi>\u03c9<\/mml:mi>\n                          <\/mml:msup>\n                        <\/mml:mrow>\n                      <\/mml:math>\n                    <\/jats:inline-formula>\n                    is logically consistent, normalizing, and that type conversion is decidable. We have mechanized all results using the Coq proof assistant.\n                  <\/jats:p>","DOI":"10.1145\/3704843","type":"journal-article","created":{"date-parts":[[2025,1,9]],"date-time":"2025-01-09T05:48:42Z","timestamp":1736401722000},"page":"183-209","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Consistency of a Dependent Calculus of Indistinguishability"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0009-0006-8717-2498","authenticated-orcid":false,"given":"Yiyun","family":"Liu","sequence":"first","affiliation":[{"name":"University of Pennsylvania, Philadelphia, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0830-3180","authenticated-orcid":false,"given":"Jonathan","family":"Chan","sequence":"additional","affiliation":[{"name":"University of Pennsylvania, Philadelphia, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6756-9168","authenticated-orcid":false,"given":"Stephanie","family":"Weirich","sequence":"additional","affiliation":[{"name":"University of Pennsylvania, Philadelphia, USA"}]}],"member":"320","published-online":{"date-parts":[[2025,1,9]]},"reference":[{"key":"e_1_3_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/292540.292555"},{"key":"e_1_3_2_3_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796819000170"},{"issue":"2","key":"e_1_3_2_4_1","article-title":"Failure of Normalization in Impredicative Type Theory with Proof-Irrelevant Propositional Equality","volume":"16","author":"Abel Andreas","year":"2020","unstructured":"Andreas Abel and Thierry Coquand. 2020. Failure of Normalization in Impredicative Type Theory with Proof-Irrelevant Propositional Equality. Logical Methods in Computer Science Volume 16, Issue 2 (June 2020), 14:1-14:5. https:\/\/doi.org\/10.23638\/lmcs-16(2:14)2020 10.23638\/lmcs-16(2:14)2020","journal-title":"Logical Methods in Computer Science"},{"key":"e_1_3_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3607862"},{"key":"e_1_3_2_6_1","first-page":"29","article-title":"Decidability of Conversion for Type Theory in Type Theory","volume":"2","author":"Abel Andreas","year":"2017","unstructured":"Andreas Abel, Joakim \u00d6hman, and Andrea Vezzosi. 2017. Decidability of Conversion for Type Theory in Type Theory. Proc. ACM Program. Lang. 2, POPL, Article 23 (Dec. 2017), 29 pages. https:\/\/doi.org\/10.1145\/3158111 10.1145\/3158111","journal-title":"Proc. ACM Program. Lang."},{"issue":"1","key":"e_1_3_2_7_1","first-page":"1","article-title":"On Irrelevance and Algorithmic Equality in Predicative Type Theory","volume":"8","author":"Abel Andreas","year":"2012","unstructured":"Andreas Abel and Gabriel Scherer. 2012. On Irrelevance and Algorithmic Equality in Predicative Type Theory. Logical Methods in Computer Science 8, 1 (2012), 1\u201336. https:\/\/doi.org\/10.2168\/lmcs-8(1:29)2012 10.2168\/lmcs-8(1:29)2012","journal-title":"Logical Methods in Computer Science"},{"key":"e_1_3_2_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-34175-6_9"},{"key":"e_1_3_2_9_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796805005770"},{"key":"e_1_3_2_10_1","first-page":"230","volume-title":"Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs(CPP 2024)","author":"Adjedj Arthur","year":"2024","unstructured":"Arthur Adjedj, Meven Lennon-Bertrand, Kenji Maillard, Pierre-Marie P\u00e9drot, and Lo\u00efc Pujet. 2024. Martin-L\u00f6f \u00e0 la Coq. In Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs (London, UK) (CPP 2024). Association for Computing Machinery, New York, NY, USA, 230\u2013245. https:\/\/doi.org\/10.1145\/3636501.3636951 10.1145\/3636501.3636951"},{"key":"e_1_3_2_11_1","unstructured":"Agda Development Team. 2023. Agda. Programming Logic Group. https:\/\/wiki.portal.chalmers.se\/agda\/Main\/HomePage"},{"key":"e_1_3_2_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08970-6_3"},{"key":"e_1_3_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209189"},{"key":"e_1_3_2_14_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/14.4.447"},{"key":"e_1_3_2_15_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796800020025"},{"key":"e_1_3_2_16_1","unstructured":"Bruno Barras. 1996. Coq en Coq. Ph. D. Dissertation. INRIA."},{"key":"e_1_3_2_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78499-9_26"},{"key":"e_1_3_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2544174.2500577"},{"key":"e_1_3_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434331"},{"key":"e_1_3_2_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99336-8_15"},{"key":"e_1_3_2_21_1","volume-title":"Implementing Mathematics with the Nuprl Proof Development System","author":"Constable R. L.","year":"1986","unstructured":"R. L. Constable, S. F. Allen, H. M. Bromley, W. R. Cleaveland, J. F. Cremer, R. W. Harper, D. J. Howe, T. B. Knoblock, N. P. Mendler, P. Panangaden, J. T. Sasaki, and S. F. Smith. 1986. Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall, Inc., USA."},{"key":"e_1_3_2_22_1","unstructured":"Coq Development Team. 2019. The Coq Proof Assistant. INRIA. https:\/\/doi.org\/10.5281\/zenodo.3476303 10.5281\/zenodo.3476303"},{"key":"e_1_3_2_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21401-6_26"},{"key":"e_1_3_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500582"},{"key":"e_1_3_2_25_1","first-page":"14","volume-title":"International Workshop on Types for Proofs and Programs","year":"1994","unstructured":"Herman Geuvers. 1994. A short and flexible proof of strong normalization for the calculus of constructions. In International Workshop on Types for Proofs and Programs. Springer, Berlin, Heidelberg, 14\u201338. https:\/\/doi.org\/10.1007\/3-540-60579-7_2 10.1007\/3-540-60579-7_2"},{"key":"e_1_3_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290316"},{"key":"e_1_3_2_27_1","unstructured":"Jean-Yves Girard Paul Taylor and Yves Lafont. 1989. Proofs and types. Vol. 7. Cambridge University Press Cambridge."},{"key":"e_1_3_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632886"},{"key":"e_1_3_2_29_1","unstructured":"Yiyun Liu Jonathan Chan and Stephanie Weirich. 2024a. Artifact associated with Consistency of a Dependent Calculus of Indistinguishability. https:\/\/doi.org\/10.5281\/zenodo.14252132 10.5281\/zenodo.14252132"},{"key":"e_1_3_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3607852"},{"key":"e_1_3_2_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-30936-1_12"},{"key":"e_1_3_2_32_1","article-title":"Quotient types via coequalizers in Martin-L\u00f6f type theory","volume":"349","author":"Mendler Nax Paul","year":"1990","unstructured":"Nax Paul Mendler. 1990. Quotient types via coequalizers in Martin-L\u00f6f type theory. In First workshop on logical frameworks. INRIA, France, 349.","journal-title":"First workshop on logical frameworks"},{"key":"e_1_3_2_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45413-6_27"},{"key":"e_1_3_2_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78499-9_25"},{"key":"e_1_3_2_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-72019-3_17"},{"key":"e_1_3_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/75277.75285"},{"key":"e_1_3_2_37_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2001.932499"},{"key":"e_1_3_2_38_1","unstructured":"932499"},{"key":"e_1_3_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498693"},{"key":"e_1_3_2_40_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796812000044"},{"key":"e_1_3_2_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/3474834"},{"key":"e_1_3_2_42_1","article-title":"Sheaf Semantics of Termination-Insensitive Noninterference","author":"Sterling Jonathan","year":"2022","unstructured":"Jonathan Sterling and Robert Harper. 2022. Sheaf Semantics of Termination-Insensitive Noninterference. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Schloss Dagstuhl-Leibniz-Zentrum f\u00fcr Informatik.","journal-title":"7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)"},{"key":"e_1_3_2_43_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1995.1057"},{"key":"e_1_3_2_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/3408973"},{"key":"e_1_3_2_45_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-4(3:13)2008"},{"key":"e_1_3_2_46_1","first-page":"266","volume-title":"Proceedings ofthe7thACMSIGPLANInternational Conference on CertifiedPrograms and Proofs(CPP 2018)","author":"Wieczorek Pawel","year":"2018","unstructured":"Pawel Wieczorek and Dariusz Biernacki. 2018. A Coq Formalization of Normalization by Evaluation for Martin-L\u00f6f Type Theory. In Proceedings ofthe7thACMSIGPLANInternational Conference on CertifiedPrograms and Proofs (Los Angeles, CA, USA) (CPP 2018). Association for Computing Machinery, New York, NY, USA, 266\u2013;279. https:\/\/doi.org\/10.1145\/3167091 10.1145\/3167091"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704843","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3704843","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T10:14:50Z","timestamp":1770200090000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704843"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,1,7]]},"references-count":45,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2025,1,7]]}},"alternative-id":["10.1145\/3704843"],"URL":"https:\/\/doi.org\/10.1145\/3704843","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,1,7]]},"assertion":[{"value":"2024-07-11","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-11-07","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-01-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}