Before revision: Soundness The soundness of a security type system can be informally defined as: If program P is well typed, P satisfies non-interference
After revision: .Soundness The soundness of a security type system can be informally defined as: If program P is well typed, P satisfies non-interference