Semantics of declassification in higher-order languages

and using purpose-built logical-relations semantics, we can reason about declassification in new ways while fully supporting higher-order programs.
To support this claim, I will study two different styles of declassification and their semantics. In the first part of my thesis, I will show how to
reason about where declassification, an intensional declassification policy, in the higher-order setting
by adapting logical relations techniques developed for noninterference. This approach leads to the first
compositional semantics for an intensional declassification policy in the higher-order setting.
In the second part of my thesis, I turn towards a style of declassification that has already been more
extensively studied in the higher-order setting using logical relation semantics: what declassification. I
will present a new approach to what declassification in higher-order languages. Specifically, I will
present a novel dependency analysis using a dependent type system and show that what-declassification
guarantees can be obtained from this dependency analysis using logical relations semantics.