Internalizing Indistinguishability with Dependent Types

Reference. Internalizing Indistinguishability with Dependent Types

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.

Cite

Cite as @liu-2024-internalizing (helia, typst) · \cite{liu-2024-internalizing} (LaTeX)

BibTeX

bibtex · 1 line

@article{liu-2024-internalizing, title={Internalizing Indistinguishability with Dependent Types}, volume={8}, ISSN={2475-1421}, url={http://dx.doi.org/10.1145/3632886}, DOI={10.1145/3632886}, number={POPL}, journal={Proceedings of the ACM on Programming Languages}, publisher={Association for Computing Machinery (ACM)}, author={Liu, Yiyun and Chan, Jonathan and Shi, Jessica and Weirich, Stephanie}, year={2024}, month=Jan, pages={1298–1325} }

hayagriva YAML (typst)

yaml · 20 lines

liu-2024-internalizing:
  type: article
  title: Internalizing Indistinguishability with Dependent Types
  author:
  - Liu, Yiyun
  - Chan, Jonathan
  - Shi, Jessica
  - Weirich, Stephanie
  date: 2024-01
  page-range: 1298-1325
  url: http://dx.doi.org/10.1145/3632886
  serial-number:
    doi: 10.1145/3632886
    issn: 2475-1421
  parent:
    type: periodical
    title: Proceedings of the ACM on Programming Languages
    publisher: Association for Computing Machinery (ACM)
    issue: POPL
    volume: 8

Download: liu-2024-internalizing.bib · liu-2024-internalizing.yml

Cited by (3)

Internalizing Extensions in Lattices of Type Theories chan-2025-internalizingarXiv · 2025

Many proof assistants allow the use of features and axioms that increase their expressive power. However, these extensions must be used with care, as some combinations are known to lead to logical inconsistencies. Therefore, proof assistants include mechanisms that track which extensions are used in a proof development or module, ensuring that incompatible extensions are not used simultaneously. Unfortunately, existing extension tracking mechanisms are external to the type system. This means that we cannot specify precisely which extensions a definition depends on. Having the ability to write more precise specifications means we are not picking an overapproximation of the extensions needed, which prevents reusing definitions in the presence of incompatible extensions. Furthermore, we cannot refer to definitions that use incompatible extensions even if they are never used in inconsistent ways. The reasoning principles of one extension therefore cannot be used as a metatheory to reason about the properties of an incompatible extension. In this report, I explore the use of the Dependent Calculus of Indistinguishability (DCOI) by Liu et al. for extension tracking. DCOI is a dependent type system with dependency tracking, where terms and variables are assigned dependency levels alongside their types. These dependency levels form a lattice that describes which levels are permitted to access what. To instead track extensions, each set of extensions would correspond to a dependency level, and the lattice would describe how extensions are permitted to interact.

arXiv

Structural Information Flow: A Fresh Look at Types for Non-interference gouni-2025-structuralOOPSLA · 2025

Information flow control is a long-studied approach for establishing non-interference properties of programs. For instance, it can be used to prove that a secret does not interfere with some computation, thereby establishing that the former does not leak through the latter. Despite their potential as a holy grail for security reasoning and their maturity within the literature, information flow type systems have seen limited adoption. In practice, information flow specifications tend to be excessively complex and can easily spiral out of control even for simple programs. Additionally, while non-interference is well-behaved in an idealized setting where information leakage never occurs, most practical programs must violate non-interference in order to fulfill their purpose. Useful information flow type systems in prior work must therefore contend with a definition of non-interference extended with declassification, which often offers weaker modular reasoning properties. We introduce structural information flow, which both illuminates and addresses these issues from a logical viewpoint. In particular, we draw on established insights from the modal logic literature to argue that information flow reasoning arises from hybrid logic, rather than conventional modal logic as previously imagined. We show with a range of examples that structural information flow specifications are straightforward to write and easy to visually parse. Uniquely in the structural setting, we demonstrate that declassification emerges not as an aberration to non-interference, but as a natural and unavoidable consequence of sufficiently general machinery for information flow. This flavor of declassification features excellent local reasoning and enables our approach to account for real-world information flow needs without compromising its theoretical elegance. Finally, we establish non-interference via a logical relations approach, showing off its simplicity in the face of the expressive power captured.

PDF · DOI · pldb

Consistency of a Dependent Calculus of Indistinguishability liu-2025-consistencyPOPL · 2025

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. 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 DCOI ω , which has an infinite predicative universe hierarchy. We show that DCOI ω is logically consistent, normalizing, and that type conversion is decidable. We have mechanized all results using the Coq proof assistant.

PDF · DOI · pldb

Cites 33 works (3 here)

With notes (3)

Logical Relations as Types: Proof-Relevant Parametricity for Program Modules sterling_harper_2021JACM · 2021

The theory of program modules is of interest to language designers not only for its practical importance to programming, but also because it lies at the nexus of three fundamental concerns in language design: the phase distinction, computational effects, and type abstraction. We contribute a fresh “synthetic” take on program modules that treats modules as the fundamental constructs, in which the usual suspects of prior module calculi (kinds, constructors, dynamic programs) are rendered as derived notions in terms of a modal type-theoretic account of the phase distinction. We simplify the account of type abstraction (embodied in the generativity of module functors) through a lax modality that encapsulates computational effects, placing projectibility of module expressions on a type-theoretic basis.

Our main result is a (significant) proof-relevant and phase-sensitive generalization of the Reynolds abstraction theorem for a calculus of program modules, based on a new kind of logical relation called a parametricity structure. Parametricity structures generalize the proof-irrelevant relations of classical parametricity to proof-relevant families, where there may be non-trivial evidence witnessing the relatedness of two programs—simplifying the metatheory of strong sums over the collection of types, for although there can be no “relation classifying relations,” one easily accommodates a “family classifying small families.”

Using the insight that logical relations/parametricity is itself a form of phase distinction between the syntactic and the semantic, we contribute a new synthetic approach to phase separated parametricity based on the slogan logical relations as types, by iterating our modal account of the phase distinction. We axiomatize a dependent type theory of parametricity structures using two pairs of complementary modalities (syntactic, semantic) and (static, dynamic), substantiated using the topos theoretic Artin gluing construction. Then, to construct a simulation between two implementations of an abstract type, one simply programs a third implementation whose type component carries the representation invariant.

DOI · arXiv

Syntax and Semantics of Quantitative Type Theory atkey-2018-syntaxLICS · 2018

DOI

I Got Plenty o’ Nuttin’ mcbride-2016-iA List of Successes That Can Change the World · 2016

DOI

External (30)

Artifact associated with Internalizing Indistinguishability with Dependent Types (2024)
Two-level type theory and applications (2023)
A dependent dependency calculus (2022)
Staged compilation with two-level type theory (2022)
Idris 2: Quantitative Type Theory in Practice (2021)
An existential crisis resolved: type inference for first-class existential types (2021)
A unified view of modalities in type systems (2020)
A graded dependent type system with a usage-aware semantics (2020)
Graded Modal Dependent Type Theory (2020)
Definitional proof-irrelevance without K (2019)
On Irrelevance and Algorithmic Equality in Predicative Type Theory (2012)
Erasure and Polymorphism in Pure Type Systems (2008)
Proving noninterference by a fully complete translation to the simply typed λ-calculus (2007)
Practical implementation of a dependently typed functional programming language (2005)
Translating dependency into parametricity (2004)
Language-based information-flow security (2003)
The implicit calculus of constructions: extending pure type systems with an intersection type binder and subtyping (2001)
Intensionality, extensionality, and proof irrelevance in modal type theory (2001)
A core calculus of dependency (1999)
Multi-stage programming with explicit annotations (1997)
A computational formalization for partial evaluation (1996)
Some extensions of Automath : the AUT-4 family (1994)
Lambda Calculi with Types (1993)
Introduction to generalized type systems (1991)
Inductively defined types (1990)
Extracting ω's programs from proofs in the calculus of constructions (1989)
Certification of programs for secure information flow (1977)
An Intuitionistic Theory of Types: Predicative Part (1975)
Interprétation fonctionnelle et élimination des coupures de l’arithmétique d’ordre supérieur (1972)
Type safe abstractions using program generators