Fine-grained information flow analysis for a ~ -calculus with sum types
Vincent Simonet · 2005
This paper presents a new type system tracing information flow for a λ-calculus equipped with polymorphic “let ” and with sums (a.k.a. union types or polymorphic variants). The type system allows establishing (weak) noninterference properties. Thanks to original forms of security annotations and constraints, it is more accurate than existing analyses. Through a straightforward encoding into sums, this work also provides a new type-based information flow analysis for programming languages featuring exceptions. From these systems, one may derive constraint-based formulations, in the style of HM(X), which have decidable type inference. 1