Noninterference in a predicative polymorphic calculus for access control
A denotational semantics based on Henkin models is given for a predicative polymorphic calculus of access control. Noninterference as a basic semantic notion of security is semantically defined. It is proven that the language is type-sound in the sense that every welltyped program of the language satisfies noninterference.
noninterference predicative polymorphism access control denotational semantics