Consistency of a Dependent Calculus of Indistinguishability

Explore a 20-minute conference talk from POPL 2025 that presents research on the consistency of the Dependent Calculus of Indistinguishability (DCOI). The presentation by researchers Yiyun Liu, Jonathan Chan, and Stephanie Weirich from the University of Pennsylvania demonstrates how DCOI uses dependency tracking to identify irrelevant arguments and employs indistinguishability during type conversion to enable proof irrelevance. Learn about how this system supports both run-time and compile-time irrelevance through a uniform mechanism and internalizes reasoning about indistinguishability via a propositional equality type indexed by observer level. The researchers identify a suitable instance called DCOIω with an infinite predicative universe hierarchy and prove it is logically consistent, normalizing, with decidable type conversion. All results have been mechanized using the Coq proof assistant and are available as reusable artifacts. The talk includes discussion of modes, dependent types, formalization, and is accompanied by supplementary materials available through Zenodo.