Research specification for confidentiality-labelled information flow in type systems, with explicit audited declassification and declassification-aware noninterference as the proof target. Specification-stage only; no checker or runtime.
type-theory programming-languages formal-methods confidentiality computer-security information-flow-control security-research information-flow type-systems language-based-security noninterference lattice-theory declassification security-types
-
Updated
Oct 4, 2026 - Shell