Internalizing Indistinguishability with Dependent TypesRemote
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 indistinguishability: 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.
Fri 19 JanDisplayed time zone: London change
10:30 - 11:50 | |||
10:30 20mTalk | Internal parametricity, without an interval POPL Thorsten Altenkirch University of Nottingham, Yorgo Chamoun École Polytechnique, Ambrus Kaposi Eötvös Loránd University, Michael Shulman University of San Diego Pre-print | ||
10:50 20mTalk | Internal and Observational Parametricity for Cubical Agda POPL | ||
11:10 20mTalk | Internalizing Indistinguishability with Dependent TypesRemote POPL Yiyun Liu University of Pennsylvania, Jonathan Chan University of Pennsylvania, Jessica Shi University of Pennsylvania, Stephanie Weirich University of Pennsylvania | ||
11:30 20mTalk | Polynomial Time and Dependent types POPL Robert Atkey University of Strathclyde |