[1]} present a translation of noninterference into parametricity with a compiler from the Dependency Core Calculus (DCC) [2]} to System F\(\omega \) . In a recent (as yet unpublished) article, [3]} extend this work to support translating declassification policies, inspired by prior work on type-based relaxed noninterference [4]}. They first provide a translation into abstract types
of the polymorphic lambda calculus [5]}, and then into signatures of a module calculus [6]}.
While that work and ours encode declassification policies via existential types (module signatures), we focus on providing a surface language for information flow control with type-based declassification. In particular, their translated programs do not support computing with secrets, which is enabled in both this work and the original work of [4]} thanks to faceted types. Additionally, they only model first-order secrets (integers), while our modular reasoning principle seamlessly accommodates higher-order secrets.
