{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:14:58Z","timestamp":1767928498177,"version":"3.49.0"},"reference-count":33,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2024,1,2]],"date-time":"2024-01-02T00:00:00Z","timestamp":1704153600000},"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":[[2024,1,2]]},"abstract":"<jats:p>\n            In type systems with dependency tracking, programmers can assign an ordered set of levels to computations and prevent information flow from high-level computations to the low-level ones. The key notion in such systems is\n            <jats:italic toggle=\"yes\">indistinguishability<\/jats:italic>\n            : a definition of program equivalence that takes into account the parts of the program that an observer may depend on. In this paper, we investigate the use of dependency tracking in the context of dependently-typed languages. We present the Dependent Calculus of Indistinguishability (DCOI), a system that adopts indistinguishability as the definition of equality used by the type checker. DCOI also internalizes that relation as an observer-indexed propositional equality type, so that programmers may reason about indistinguishability within the language. Our design generalizes and extends prior systems that combine dependency tracking with dependent types and is the first to support conversion and propositional equality at arbitrary observer levels. We have proven type soundness and noninterference theorems for DCOI and have developed a prototype implementation of its type checker.\n          <\/jats:p>","DOI":"10.1145\/3632886","type":"journal-article","created":{"date-parts":[[2024,1,5]],"date-time":"2024-01-05T20:48:51Z","timestamp":1704487731000},"page":"1298-1325","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Internalizing Indistinguishability with Dependent Types"],"prefix":"10.1145","volume":"8","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"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0830-3180","authenticated-orcid":false,"given":"Jonathan","family":"Chan","sequence":"additional","affiliation":[{"name":"University of Pennsylvania, Philadelphia, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1507-1122","authenticated-orcid":false,"given":"Jessica","family":"Shi","sequence":"additional","affiliation":[{"name":"University of Pennsylvania, Philadelphia, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6756-9168","authenticated-orcid":false,"given":"Stephanie","family":"Weirich","sequence":"additional","affiliation":[{"name":"University of Pennsylvania, Philadelphia, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2024,1,5]]},"reference":[{"key":"e_1_3_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/292540.292555"},{"key":"e_1_3_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3408972"},{"key":"e_1_3_1_4_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-8(1:29)2012"},{"key":"e_1_3_1_5_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129523000130"},{"key":"e_1_3_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209189"},{"key":"e_1_3_1_7_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796800020025"},{"key":"e_1_3_1_8_1","first-page":"117","volume-title":"Lambda Calculi with Types","author":"Barendregt Henk P.","year":"1993","unstructured":"Henk P. Barendregt. 1993. Lambda Calculi with Types. Oxford University Press, Inc., USA, 117\u2013309."},{"key":"e_1_3_1_9_1","volume-title":"Practical implementation of a dependently typed functional programming language","author":"Brady Edwin C.","year":"2005","unstructured":"Edwin C. Brady. 2005. Practical implementation of a dependently typed functional programming language. Ph. D. Dissertation. Durham University, UK. http:\/\/etheses.dur.ac.uk\/2800\/"},{"key":"e_1_3_1_10_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2021.9"},{"key":"e_1_3_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99336-8_15"},{"key":"e_1_3_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434331"},{"key":"e_1_3_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-52335-9_47"},{"key":"e_1_3_1_14_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)70209-X"},{"key":"e_1_3_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/359636.359712"},{"key":"e_1_3_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3473569"},{"key":"e_1_3_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290316"},{"key":"e_1_3_1_18_1","volume-title":"Interpr\u00e9tation fonctionnelle et \u00e9limination des coupures de l\u2019arithm\u00e9tique d\u2019ordre sup\u00e9rieur","author":"Girard Jean-Yves","year":"1972","unstructured":"Jean-Yves Girard. 1972. Interpr\u00e9tation fonctionnelle et \u00e9limination des coupures de l\u2019arithm\u00e9tique d\u2019ordre sup\u00e9rieur. Ph. D. Dissertation. Universit\u00e9 Paris 7."},{"key":"e_1_3_1_19_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129597002405"},{"key":"e_1_3_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3547641"},{"key":"e_1_3_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3580424"},{"key":"e_1_3_1_22_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)71945-1"},{"key":"e_1_3_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-30936-1_12"},{"key":"e_1_3_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45413-6_27"},{"key":"e_1_3_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78499-9_25"},{"key":"e_1_3_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-72019-3_17"},{"key":"e_1_3_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/75277.75285"},{"key":"e_1_3_1_28_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2001.932499"},{"key":"e_1_3_1_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/JSAC.2002.806121"},{"key":"e_1_3_1_30_1","doi-asserted-by":"publisher","DOI":"10.6083\/w95050724"},{"key":"e_1_3_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-77505-8_24"},{"key":"e_1_3_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3474834"},{"key":"e_1_3_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/258993.259019"},{"key":"e_1_3_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/1016848.1016868"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632886","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3632886","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3632886","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:06:20Z","timestamp":1751659580000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632886"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,1,2]]},"references-count":33,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2024,1,2]]}},"alternative-id":["10.1145\/3632886"],"URL":"https:\/\/doi.org\/10.1145\/3632886","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,1,2]]},"assertion":[{"value":"2024-01-05","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}