Internalizing Indistinguishability with Dependent Types

Explore a groundbreaking 20-minute conference talk from POPL 2024 that delves into the Dependent Calculus of Indistinguishability (DCOI), a novel system combining dependency tracking with dependent types. Learn how researchers from the University of Pennsylvania have developed a type system that internalizes indistinguishability as the definition of equality used by the type checker, allowing programmers to reason about indistinguishability within the language itself. Discover how DCOI supports conversion and propositional equality at arbitrary observer levels, extending prior systems in this field. Gain insights into the type soundness and noninterference theorems proven for DCOI, and learn about the prototype implementation of its type checker. This talk is ideal for those interested in type systems, dependent types, information flow control, and formal verification in programming languages.