Subtyping:
- τ <: τ' means τ' is a higher security class than τ (e.g. L <: H)
- τ var <: τ' var if τ <: τ' (covariant)
- τ' cmd <: τ cmd if τ <: τ' (contravariant)
- Subtyping is reflexive (and transitive). All types are subtypes of themselves (τ <: τ)
Allows for more complex set of security classes (e.g. {H,L1,L2 | L1 <: H & L2 <: H}