  Language-based information flow control (IFC) tracks dependencies within a
program using sensitivity labels and prohibits public outputs from depending on
secret inputs. In particular, literature has proposed several type systems for
tracking these dependencies. On one extreme, there are fine-grained type
systems (like Flow Caml) that label all values individually and track
dependence at the level of individual values. On the other extreme are
coarse-grained type systems (like HLIO) that track dependence coarsely, by
associating a single label with an entire computation context and not labeling
all values individually.
  In this paper, we show that, despite their glaring differences, both these
styles are, in fact, equally expressive. To do this, we show a semantics- and
type-preserving translation from a coarse-grained type system to a fine-grained
one and vice-versa. The forward translation isn't surprising, but the backward
translation is: It requires a construct to arbitrarily limit the scope of a
context label in the coarse-grained type system (e.g., HLIO's "toLabeled"
construct). As a separate contribution, we show how to extend work on logical
relation models of IFC types to higher-order state. We build such logical
relations for both the fine-grained type system and the coarse-grained type
system. We use these relations to prove the two type systems and our
translations between them sound.
