  Information-flow security type systems ensure confidentiality by enforcing
noninterference: a program cannot leak private data to public channels.
However, in practice, programs need to selectively declassify information about
private data. Several approaches have provided a notion of relaxed
noninterference supporting selective and expressive declassification while
retaining a formal security property. The labels-as-functions approach provides
relaxed noninterference by means of declassification policies expressed as
functions. The labels-as-types approach expresses declassification policies
using type abstraction and faceted types, a pair of types representing the
secret and public facets of values. The original proposal of labels-as-types is
formulated in an object-oriented setting where type abstraction is realized by
subtyping. The object-oriented approach however suffers from limitations due to
its receiver-centric paradigm.
  In this work, we consider an alternative approach to labels-as-types,
applicable in non-object-oriented languages, which allows us to express
advanced declassification policies, such as extrinsic policies, based on a
different form of type abstraction: existential types. An existential type
exposes abstract types and operations on these; we leverage this abstraction
mechanism to express secrets that can be declassified using the provided
operations. We formalize the approach in a core functional calculus with
existential types, define existential relaxed noninterference, and prove that
well-typed programs satisfy this form of type-based relaxed noninterference.
